YES 10.054
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ IFR
mainModule Main
| ((gcd :: Int -> Int -> Int) :: Int -> Int -> Int) |
module Main where
If Reductions:
The following If expression
if primGEqNatS x y then primModNatS (primMinusNatS x y) (Succ y) else Succ x
is transformed to
primModNatS0 | x y True | = primModNatS (primMinusNatS x y) (Succ y) |
primModNatS0 | x y False | = Succ x |
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
mainModule Main
| ((gcd :: Int -> Int -> Int) :: Int -> Int -> Int) |
module Main where
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule Main
| ((gcd :: Int -> Int -> Int) :: Int -> Int -> Int) |
module Main where
Cond Reductions:
The following Function with conditions
gcd' | x 0 | = x |
gcd' | x y | = gcd' y (x `rem` y) |
is transformed to
gcd' | x xx | = gcd'2 x xx |
gcd' | x y | = gcd'0 x y |
gcd'0 | x y | = gcd' y (x `rem` y) |
gcd'1 | True x xx | = x |
gcd'1 | xy xz yu | = gcd'0 xz yu |
gcd'2 | x xx | = gcd'1 (xx == 0) x xx |
gcd'2 | yv yw | = gcd'0 yv yw |
The following Function with conditions
gcd | 0 0 | = error [] |
gcd | x y | =
gcd' (abs x) (abs y) |
where |
gcd' | x 0 | = x |
gcd' | x y | = gcd' y (x `rem` y) |
|
|
is transformed to
gcd | yx yy | = gcd3 yx yy |
gcd | x y | = gcd0 x y |
gcd0 | x y | =
gcd' (abs x) (abs y) |
where |
gcd' | x xx | = gcd'2 x xx |
gcd' | x y | = gcd'0 x y |
|
|
gcd'0 | x y | = gcd' y (x `rem` y) |
|
|
gcd'1 | True x xx | = x |
gcd'1 | xy xz yu | = gcd'0 xz yu |
|
|
gcd'2 | x xx | = gcd'1 (xx == 0) x xx |
gcd'2 | yv yw | = gcd'0 yv yw |
|
|
gcd1 | True yx yy | = error [] |
gcd1 | yz zu zv | = gcd0 zu zv |
gcd2 | True yx yy | = gcd1 (yy == 0) yx yy |
gcd2 | zw zx zy | = gcd0 zx zy |
gcd3 | yx yy | = gcd2 (yx == 0) yx yy |
gcd3 | zz vuu | = gcd0 zz vuu |
The following Function with conditions
is transformed to
absReal0 | x True | = `negate` x |
absReal1 | x True | = x |
absReal1 | x False | = absReal0 x otherwise |
absReal2 | x | = absReal1 x (x >= 0) |
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
mainModule Main
| ((gcd :: Int -> Int -> Int) :: Int -> Int -> Int) |
module Main where
Let/Where Reductions:
The bindings of the following Let/Where expression
gcd' (abs x) (abs y) |
where |
gcd' | x xx | = gcd'2 x xx |
gcd' | x y | = gcd'0 x y |
|
|
gcd'0 | x y | = gcd' y (x `rem` y) |
|
|
gcd'1 | True x xx | = x |
gcd'1 | xy xz yu | = gcd'0 xz yu |
|
|
gcd'2 | x xx | = gcd'1 (xx == 0) x xx |
gcd'2 | yv yw | = gcd'0 yv yw |
|
are unpacked to the following functions on top level
gcd0Gcd' | x xx | = gcd0Gcd'2 x xx |
gcd0Gcd' | x y | = gcd0Gcd'0 x y |
gcd0Gcd'1 | True x xx | = x |
gcd0Gcd'1 | xy xz yu | = gcd0Gcd'0 xz yu |
gcd0Gcd'2 | x xx | = gcd0Gcd'1 (xx == 0) x xx |
gcd0Gcd'2 | yv yw | = gcd0Gcd'0 yv yw |
gcd0Gcd'0 | x y | = gcd0Gcd' y (x `rem` y) |
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
mainModule Main
| ((gcd :: Int -> Int -> Int) :: Int -> Int -> Int) |
module Main where
Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
mainModule Main
| (gcd :: Int -> Int -> Int) |
module Main where
Haskell To QDPs
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMinusNatS(Succ(vuv230), Succ(vuv2400)) → new_primMinusNatS(vuv230, vuv2400)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMinusNatS(Succ(vuv230), Succ(vuv2400)) → new_primMinusNatS(vuv230, vuv2400)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'18(vuv78, vuv79, Zero, Succ(vuv810)) → new_gcd0Gcd'12(Succ(vuv78), Neg(Succ(vuv79)))
new_gcd0Gcd'0(Pos(Succ(Succ(vuv6000))), Zero) → new_gcd0Gcd'11(vuv6000, Zero)
new_gcd0Gcd'15(vuv29, vuv30) → new_gcd0Gcd'17(Succ(vuv30), vuv29, Succ(vuv30))
new_gcd0Gcd'1(Succ(Zero), Zero) → new_gcd0Gcd'1(new_primMinusNatS0, Zero)
new_gcd0Gcd'16(Succ(Succ(vuv6000)), Zero) → new_gcd0Gcd'14(vuv6000, Zero)
new_gcd0Gcd'16(Succ(Zero), Succ(vuv4000)) → new_gcd0Gcd'15(Zero, Succ(vuv4000))
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430)
new_gcd0Gcd'11(vuv23, vuv24) → new_gcd0Gcd'1(new_primMinusNatS1(vuv23, vuv24), vuv24)
new_gcd0Gcd'0(Pos(Succ(Zero)), Zero) → new_gcd0Gcd'1(new_primMinusNatS0, Zero)
new_gcd0Gcd'17(Succ(Zero), Zero, vuv63) → new_gcd0Gcd'17(new_primMinusNatS2(Zero, Zero), Zero, new_primMinusNatS2(Zero, Zero))
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810)
new_gcd0Gcd'16(Succ(Succ(vuv6000)), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'17(Succ(Zero), Succ(vuv620), vuv63) → new_gcd0Gcd'12(Zero, Neg(Succ(Succ(vuv620))))
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Succ(vuv620), vuv63) → new_gcd0Gcd'18(vuv6400, Succ(vuv620), vuv6400, vuv620)
new_gcd0Gcd'12(vuv400, vuv5) → new_gcd0Gcd'0(vuv5, vuv400)
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'18(vuv78, vuv79, Zero, Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'10(vuv35, vuv36, Zero, Zero) → new_gcd0Gcd'11(vuv35, vuv36)
new_gcd0Gcd'0(Neg(Succ(Zero)), Zero) → new_gcd0Gcd'16(new_primMinusNatS0, Zero)
new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Succ(vuv380)) → new_gcd0Gcd'10(vuv35, vuv36, vuv370, vuv380)
new_gcd0Gcd'0(Pos(Succ(Zero)), Succ(vuv4000)) → new_gcd0Gcd'12(Zero, Pos(Succ(Succ(vuv4000))))
new_gcd0Gcd'16(Succ(Zero), Zero) → new_gcd0Gcd'16(new_primMinusNatS0, Zero)
new_gcd0Gcd'1(Succ(Succ(vuv6000)), Zero) → new_gcd0Gcd'11(vuv6000, Zero)
new_gcd0Gcd'13(vuv40, vuv41, Zero, Succ(vuv430)) → new_gcd0Gcd'15(Succ(vuv40), vuv41)
new_gcd0Gcd'10(vuv35, vuv36, Zero, Succ(vuv380)) → new_gcd0Gcd'12(Succ(vuv35), Pos(Succ(vuv36)))
new_gcd0Gcd'13(vuv40, vuv41, Zero, Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'1(Succ(Zero), Succ(vuv4000)) → new_gcd0Gcd'12(Zero, Pos(Succ(Succ(vuv4000))))
new_gcd0Gcd'0(Pos(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'0(Neg(Succ(Zero)), Succ(vuv4000)) → new_gcd0Gcd'15(Zero, Succ(vuv4000))
new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Zero) → new_gcd0Gcd'11(vuv35, vuv36)
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Zero) → new_gcd0Gcd'14(vuv6000, Zero)
new_gcd0Gcd'19(vuv72, vuv73) → new_gcd0Gcd'17(new_primMinusNatS2(Succ(vuv72), vuv73), vuv73, new_primMinusNatS2(Succ(vuv72), vuv73))
new_gcd0Gcd'14(vuv26, vuv27) → new_gcd0Gcd'16(new_primMinusNatS1(vuv26, vuv27), vuv27)
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Zero, vuv63) → new_gcd0Gcd'19(vuv6400, Zero)
new_gcd0Gcd'1(Succ(Succ(vuv6000)), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
The TRS R consists of the following rules:
new_primMinusNatS1(vuv23, Zero) → Succ(vuv23)
new_primMinusNatS2(Succ(vuv230), Succ(vuv2400)) → new_primMinusNatS2(vuv230, vuv2400)
new_primMinusNatS2(Zero, Succ(vuv2400)) → Zero
new_primMinusNatS1(vuv23, Succ(vuv240)) → new_primMinusNatS2(vuv23, vuv240)
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS0 → Zero
new_primMinusNatS2(Succ(vuv230), Zero) → Succ(vuv230)
The set Q consists of the following terms:
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS0
new_primMinusNatS1(x0, Succ(x1))
new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS1(x0, Zero)
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 5 less nodes.
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'18(vuv78, vuv79, Zero, Succ(vuv810)) → new_gcd0Gcd'12(Succ(vuv78), Neg(Succ(vuv79)))
new_gcd0Gcd'0(Pos(Succ(Succ(vuv6000))), Zero) → new_gcd0Gcd'11(vuv6000, Zero)
new_gcd0Gcd'15(vuv29, vuv30) → new_gcd0Gcd'17(Succ(vuv30), vuv29, Succ(vuv30))
new_gcd0Gcd'16(Succ(Succ(vuv6000)), Zero) → new_gcd0Gcd'14(vuv6000, Zero)
new_gcd0Gcd'16(Succ(Zero), Succ(vuv4000)) → new_gcd0Gcd'15(Zero, Succ(vuv4000))
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430)
new_gcd0Gcd'11(vuv23, vuv24) → new_gcd0Gcd'1(new_primMinusNatS1(vuv23, vuv24), vuv24)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810)
new_gcd0Gcd'16(Succ(Succ(vuv6000)), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'17(Succ(Zero), Succ(vuv620), vuv63) → new_gcd0Gcd'12(Zero, Neg(Succ(Succ(vuv620))))
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Succ(vuv620), vuv63) → new_gcd0Gcd'18(vuv6400, Succ(vuv620), vuv6400, vuv620)
new_gcd0Gcd'12(vuv400, vuv5) → new_gcd0Gcd'0(vuv5, vuv400)
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'18(vuv78, vuv79, Zero, Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'10(vuv35, vuv36, Zero, Zero) → new_gcd0Gcd'11(vuv35, vuv36)
new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Succ(vuv380)) → new_gcd0Gcd'10(vuv35, vuv36, vuv370, vuv380)
new_gcd0Gcd'0(Pos(Succ(Zero)), Succ(vuv4000)) → new_gcd0Gcd'12(Zero, Pos(Succ(Succ(vuv4000))))
new_gcd0Gcd'1(Succ(Succ(vuv6000)), Zero) → new_gcd0Gcd'11(vuv6000, Zero)
new_gcd0Gcd'13(vuv40, vuv41, Zero, Succ(vuv430)) → new_gcd0Gcd'15(Succ(vuv40), vuv41)
new_gcd0Gcd'13(vuv40, vuv41, Zero, Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'10(vuv35, vuv36, Zero, Succ(vuv380)) → new_gcd0Gcd'12(Succ(vuv35), Pos(Succ(vuv36)))
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'1(Succ(Zero), Succ(vuv4000)) → new_gcd0Gcd'12(Zero, Pos(Succ(Succ(vuv4000))))
new_gcd0Gcd'0(Pos(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'0(Neg(Succ(Zero)), Succ(vuv4000)) → new_gcd0Gcd'15(Zero, Succ(vuv4000))
new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Zero) → new_gcd0Gcd'11(vuv35, vuv36)
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Zero) → new_gcd0Gcd'14(vuv6000, Zero)
new_gcd0Gcd'19(vuv72, vuv73) → new_gcd0Gcd'17(new_primMinusNatS2(Succ(vuv72), vuv73), vuv73, new_primMinusNatS2(Succ(vuv72), vuv73))
new_gcd0Gcd'14(vuv26, vuv27) → new_gcd0Gcd'16(new_primMinusNatS1(vuv26, vuv27), vuv27)
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Zero, vuv63) → new_gcd0Gcd'19(vuv6400, Zero)
new_gcd0Gcd'1(Succ(Succ(vuv6000)), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
The TRS R consists of the following rules:
new_primMinusNatS1(vuv23, Zero) → Succ(vuv23)
new_primMinusNatS2(Succ(vuv230), Succ(vuv2400)) → new_primMinusNatS2(vuv230, vuv2400)
new_primMinusNatS2(Zero, Succ(vuv2400)) → Zero
new_primMinusNatS1(vuv23, Succ(vuv240)) → new_primMinusNatS2(vuv23, vuv240)
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS0 → Zero
new_primMinusNatS2(Succ(vuv230), Zero) → Succ(vuv230)
The set Q consists of the following terms:
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS0
new_primMinusNatS1(x0, Succ(x1))
new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS1(x0, Zero)
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'18(vuv78, vuv79, Zero, Succ(vuv810)) → new_gcd0Gcd'12(Succ(vuv78), Neg(Succ(vuv79)))
new_gcd0Gcd'0(Pos(Succ(Succ(vuv6000))), Zero) → new_gcd0Gcd'11(vuv6000, Zero)
new_gcd0Gcd'15(vuv29, vuv30) → new_gcd0Gcd'17(Succ(vuv30), vuv29, Succ(vuv30))
new_gcd0Gcd'16(Succ(Succ(vuv6000)), Zero) → new_gcd0Gcd'14(vuv6000, Zero)
new_gcd0Gcd'16(Succ(Zero), Succ(vuv4000)) → new_gcd0Gcd'15(Zero, Succ(vuv4000))
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430)
new_gcd0Gcd'11(vuv23, vuv24) → new_gcd0Gcd'1(new_primMinusNatS1(vuv23, vuv24), vuv24)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810)
new_gcd0Gcd'16(Succ(Succ(vuv6000)), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'17(Succ(Zero), Succ(vuv620), vuv63) → new_gcd0Gcd'12(Zero, Neg(Succ(Succ(vuv620))))
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Succ(vuv620), vuv63) → new_gcd0Gcd'18(vuv6400, Succ(vuv620), vuv6400, vuv620)
new_gcd0Gcd'12(vuv400, vuv5) → new_gcd0Gcd'0(vuv5, vuv400)
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'18(vuv78, vuv79, Zero, Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'10(vuv35, vuv36, Zero, Zero) → new_gcd0Gcd'11(vuv35, vuv36)
new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Succ(vuv380)) → new_gcd0Gcd'10(vuv35, vuv36, vuv370, vuv380)
new_gcd0Gcd'0(Pos(Succ(Zero)), Succ(vuv4000)) → new_gcd0Gcd'12(Zero, Pos(Succ(Succ(vuv4000))))
new_gcd0Gcd'1(Succ(Succ(vuv6000)), Zero) → new_gcd0Gcd'11(vuv6000, Zero)
new_gcd0Gcd'13(vuv40, vuv41, Zero, Succ(vuv430)) → new_gcd0Gcd'15(Succ(vuv40), vuv41)
new_gcd0Gcd'13(vuv40, vuv41, Zero, Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'10(vuv35, vuv36, Zero, Succ(vuv380)) → new_gcd0Gcd'12(Succ(vuv35), Pos(Succ(vuv36)))
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'1(Succ(Zero), Succ(vuv4000)) → new_gcd0Gcd'12(Zero, Pos(Succ(Succ(vuv4000))))
new_gcd0Gcd'0(Pos(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'0(Neg(Succ(Zero)), Succ(vuv4000)) → new_gcd0Gcd'15(Zero, Succ(vuv4000))
new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Zero) → new_gcd0Gcd'11(vuv35, vuv36)
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Zero) → new_gcd0Gcd'14(vuv6000, Zero)
new_gcd0Gcd'19(vuv72, vuv73) → new_gcd0Gcd'17(new_primMinusNatS2(Succ(vuv72), vuv73), vuv73, new_primMinusNatS2(Succ(vuv72), vuv73))
new_gcd0Gcd'14(vuv26, vuv27) → new_gcd0Gcd'16(new_primMinusNatS1(vuv26, vuv27), vuv27)
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Zero, vuv63) → new_gcd0Gcd'19(vuv6400, Zero)
new_gcd0Gcd'1(Succ(Succ(vuv6000)), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
The TRS R consists of the following rules:
new_primMinusNatS1(vuv23, Zero) → Succ(vuv23)
new_primMinusNatS1(vuv23, Succ(vuv240)) → new_primMinusNatS2(vuv23, vuv240)
new_primMinusNatS2(Succ(vuv230), Succ(vuv2400)) → new_primMinusNatS2(vuv230, vuv2400)
new_primMinusNatS2(Zero, Succ(vuv2400)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vuv230), Zero) → Succ(vuv230)
The set Q consists of the following terms:
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS0
new_primMinusNatS1(x0, Succ(x1))
new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS1(x0, Zero)
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
new_primMinusNatS0
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'18(vuv78, vuv79, Zero, Succ(vuv810)) → new_gcd0Gcd'12(Succ(vuv78), Neg(Succ(vuv79)))
new_gcd0Gcd'0(Pos(Succ(Succ(vuv6000))), Zero) → new_gcd0Gcd'11(vuv6000, Zero)
new_gcd0Gcd'15(vuv29, vuv30) → new_gcd0Gcd'17(Succ(vuv30), vuv29, Succ(vuv30))
new_gcd0Gcd'16(Succ(Succ(vuv6000)), Zero) → new_gcd0Gcd'14(vuv6000, Zero)
new_gcd0Gcd'16(Succ(Zero), Succ(vuv4000)) → new_gcd0Gcd'15(Zero, Succ(vuv4000))
new_gcd0Gcd'11(vuv23, vuv24) → new_gcd0Gcd'1(new_primMinusNatS1(vuv23, vuv24), vuv24)
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810)
new_gcd0Gcd'16(Succ(Succ(vuv6000)), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'17(Succ(Zero), Succ(vuv620), vuv63) → new_gcd0Gcd'12(Zero, Neg(Succ(Succ(vuv620))))
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Succ(vuv620), vuv63) → new_gcd0Gcd'18(vuv6400, Succ(vuv620), vuv6400, vuv620)
new_gcd0Gcd'12(vuv400, vuv5) → new_gcd0Gcd'0(vuv5, vuv400)
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'18(vuv78, vuv79, Zero, Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'10(vuv35, vuv36, Zero, Zero) → new_gcd0Gcd'11(vuv35, vuv36)
new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Succ(vuv380)) → new_gcd0Gcd'10(vuv35, vuv36, vuv370, vuv380)
new_gcd0Gcd'0(Pos(Succ(Zero)), Succ(vuv4000)) → new_gcd0Gcd'12(Zero, Pos(Succ(Succ(vuv4000))))
new_gcd0Gcd'1(Succ(Succ(vuv6000)), Zero) → new_gcd0Gcd'11(vuv6000, Zero)
new_gcd0Gcd'13(vuv40, vuv41, Zero, Succ(vuv430)) → new_gcd0Gcd'15(Succ(vuv40), vuv41)
new_gcd0Gcd'13(vuv40, vuv41, Zero, Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'10(vuv35, vuv36, Zero, Succ(vuv380)) → new_gcd0Gcd'12(Succ(vuv35), Pos(Succ(vuv36)))
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'1(Succ(Zero), Succ(vuv4000)) → new_gcd0Gcd'12(Zero, Pos(Succ(Succ(vuv4000))))
new_gcd0Gcd'0(Pos(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Zero) → new_gcd0Gcd'11(vuv35, vuv36)
new_gcd0Gcd'0(Neg(Succ(Zero)), Succ(vuv4000)) → new_gcd0Gcd'15(Zero, Succ(vuv4000))
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Zero) → new_gcd0Gcd'14(vuv6000, Zero)
new_gcd0Gcd'19(vuv72, vuv73) → new_gcd0Gcd'17(new_primMinusNatS2(Succ(vuv72), vuv73), vuv73, new_primMinusNatS2(Succ(vuv72), vuv73))
new_gcd0Gcd'14(vuv26, vuv27) → new_gcd0Gcd'16(new_primMinusNatS1(vuv26, vuv27), vuv27)
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Zero, vuv63) → new_gcd0Gcd'19(vuv6400, Zero)
new_gcd0Gcd'1(Succ(Succ(vuv6000)), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
The TRS R consists of the following rules:
new_primMinusNatS1(vuv23, Zero) → Succ(vuv23)
new_primMinusNatS1(vuv23, Succ(vuv240)) → new_primMinusNatS2(vuv23, vuv240)
new_primMinusNatS2(Succ(vuv230), Succ(vuv2400)) → new_primMinusNatS2(vuv230, vuv2400)
new_primMinusNatS2(Zero, Succ(vuv2400)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vuv230), Zero) → Succ(vuv230)
The set Q consists of the following terms:
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS1(x0, Succ(x1))
new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS1(x0, Zero)
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule new_gcd0Gcd'11(vuv23, vuv24) → new_gcd0Gcd'1(new_primMinusNatS1(vuv23, vuv24), vuv24) at position [0] we obtained the following new rules:
new_gcd0Gcd'11(x0, Zero) → new_gcd0Gcd'1(Succ(x0), Zero)
new_gcd0Gcd'11(x0, Succ(x1)) → new_gcd0Gcd'1(new_primMinusNatS2(x0, x1), Succ(x1))
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'18(vuv78, vuv79, Zero, Succ(vuv810)) → new_gcd0Gcd'12(Succ(vuv78), Neg(Succ(vuv79)))
new_gcd0Gcd'0(Pos(Succ(Succ(vuv6000))), Zero) → new_gcd0Gcd'11(vuv6000, Zero)
new_gcd0Gcd'15(vuv29, vuv30) → new_gcd0Gcd'17(Succ(vuv30), vuv29, Succ(vuv30))
new_gcd0Gcd'16(Succ(Succ(vuv6000)), Zero) → new_gcd0Gcd'14(vuv6000, Zero)
new_gcd0Gcd'16(Succ(Zero), Succ(vuv4000)) → new_gcd0Gcd'15(Zero, Succ(vuv4000))
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810)
new_gcd0Gcd'16(Succ(Succ(vuv6000)), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'17(Succ(Zero), Succ(vuv620), vuv63) → new_gcd0Gcd'12(Zero, Neg(Succ(Succ(vuv620))))
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Succ(vuv620), vuv63) → new_gcd0Gcd'18(vuv6400, Succ(vuv620), vuv6400, vuv620)
new_gcd0Gcd'12(vuv400, vuv5) → new_gcd0Gcd'0(vuv5, vuv400)
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'18(vuv78, vuv79, Zero, Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'10(vuv35, vuv36, Zero, Zero) → new_gcd0Gcd'11(vuv35, vuv36)
new_gcd0Gcd'11(x0, Zero) → new_gcd0Gcd'1(Succ(x0), Zero)
new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Succ(vuv380)) → new_gcd0Gcd'10(vuv35, vuv36, vuv370, vuv380)
new_gcd0Gcd'0(Pos(Succ(Zero)), Succ(vuv4000)) → new_gcd0Gcd'12(Zero, Pos(Succ(Succ(vuv4000))))
new_gcd0Gcd'1(Succ(Succ(vuv6000)), Zero) → new_gcd0Gcd'11(vuv6000, Zero)
new_gcd0Gcd'13(vuv40, vuv41, Zero, Succ(vuv430)) → new_gcd0Gcd'15(Succ(vuv40), vuv41)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'10(vuv35, vuv36, Zero, Succ(vuv380)) → new_gcd0Gcd'12(Succ(vuv35), Pos(Succ(vuv36)))
new_gcd0Gcd'13(vuv40, vuv41, Zero, Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'11(x0, Succ(x1)) → new_gcd0Gcd'1(new_primMinusNatS2(x0, x1), Succ(x1))
new_gcd0Gcd'1(Succ(Zero), Succ(vuv4000)) → new_gcd0Gcd'12(Zero, Pos(Succ(Succ(vuv4000))))
new_gcd0Gcd'0(Pos(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'0(Neg(Succ(Zero)), Succ(vuv4000)) → new_gcd0Gcd'15(Zero, Succ(vuv4000))
new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Zero) → new_gcd0Gcd'11(vuv35, vuv36)
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Zero) → new_gcd0Gcd'14(vuv6000, Zero)
new_gcd0Gcd'19(vuv72, vuv73) → new_gcd0Gcd'17(new_primMinusNatS2(Succ(vuv72), vuv73), vuv73, new_primMinusNatS2(Succ(vuv72), vuv73))
new_gcd0Gcd'14(vuv26, vuv27) → new_gcd0Gcd'16(new_primMinusNatS1(vuv26, vuv27), vuv27)
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Zero, vuv63) → new_gcd0Gcd'19(vuv6400, Zero)
new_gcd0Gcd'1(Succ(Succ(vuv6000)), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
The TRS R consists of the following rules:
new_primMinusNatS1(vuv23, Zero) → Succ(vuv23)
new_primMinusNatS1(vuv23, Succ(vuv240)) → new_primMinusNatS2(vuv23, vuv240)
new_primMinusNatS2(Succ(vuv230), Succ(vuv2400)) → new_primMinusNatS2(vuv230, vuv2400)
new_primMinusNatS2(Zero, Succ(vuv2400)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vuv230), Zero) → Succ(vuv230)
The set Q consists of the following terms:
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS1(x0, Succ(x1))
new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS1(x0, Zero)
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 1 less node.
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'1(Succ(Succ(vuv6000)), Zero) → new_gcd0Gcd'11(vuv6000, Zero)
new_gcd0Gcd'11(x0, Zero) → new_gcd0Gcd'1(Succ(x0), Zero)
The TRS R consists of the following rules:
new_primMinusNatS1(vuv23, Zero) → Succ(vuv23)
new_primMinusNatS1(vuv23, Succ(vuv240)) → new_primMinusNatS2(vuv23, vuv240)
new_primMinusNatS2(Succ(vuv230), Succ(vuv2400)) → new_primMinusNatS2(vuv230, vuv2400)
new_primMinusNatS2(Zero, Succ(vuv2400)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vuv230), Zero) → Succ(vuv230)
The set Q consists of the following terms:
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS1(x0, Succ(x1))
new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS1(x0, Zero)
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'1(Succ(Succ(vuv6000)), Zero) → new_gcd0Gcd'11(vuv6000, Zero)
new_gcd0Gcd'11(x0, Zero) → new_gcd0Gcd'1(Succ(x0), Zero)
R is empty.
The set Q consists of the following terms:
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS1(x0, Succ(x1))
new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS1(x0, Zero)
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS1(x0, Succ(x1))
new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS1(x0, Zero)
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'1(Succ(Succ(vuv6000)), Zero) → new_gcd0Gcd'11(vuv6000, Zero)
new_gcd0Gcd'11(x0, Zero) → new_gcd0Gcd'1(Succ(x0), Zero)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:
new_gcd0Gcd'1(Succ(Succ(vuv6000)), Zero) → new_gcd0Gcd'11(vuv6000, Zero)
new_gcd0Gcd'11(x0, Zero) → new_gcd0Gcd'1(Succ(x0), Zero)
Used ordering: POLO with Polynomial interpretation [25]:
POL(Succ(x1)) = 1 + 2·x1
POL(Zero) = 0
POL(new_gcd0Gcd'1(x1, x2)) = x1 + x2
POL(new_gcd0Gcd'11(x1, x2)) = 2 + 2·x1 + x2
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ PisEmptyProof
↳ QDP
Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'18(vuv78, vuv79, Zero, Succ(vuv810)) → new_gcd0Gcd'12(Succ(vuv78), Neg(Succ(vuv79)))
new_gcd0Gcd'15(vuv29, vuv30) → new_gcd0Gcd'17(Succ(vuv30), vuv29, Succ(vuv30))
new_gcd0Gcd'16(Succ(Succ(vuv6000)), Zero) → new_gcd0Gcd'14(vuv6000, Zero)
new_gcd0Gcd'16(Succ(Zero), Succ(vuv4000)) → new_gcd0Gcd'15(Zero, Succ(vuv4000))
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810)
new_gcd0Gcd'16(Succ(Succ(vuv6000)), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'17(Succ(Zero), Succ(vuv620), vuv63) → new_gcd0Gcd'12(Zero, Neg(Succ(Succ(vuv620))))
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Succ(vuv620), vuv63) → new_gcd0Gcd'18(vuv6400, Succ(vuv620), vuv6400, vuv620)
new_gcd0Gcd'12(vuv400, vuv5) → new_gcd0Gcd'0(vuv5, vuv400)
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'18(vuv78, vuv79, Zero, Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'10(vuv35, vuv36, Zero, Zero) → new_gcd0Gcd'11(vuv35, vuv36)
new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Succ(vuv380)) → new_gcd0Gcd'10(vuv35, vuv36, vuv370, vuv380)
new_gcd0Gcd'0(Pos(Succ(Zero)), Succ(vuv4000)) → new_gcd0Gcd'12(Zero, Pos(Succ(Succ(vuv4000))))
new_gcd0Gcd'13(vuv40, vuv41, Zero, Succ(vuv430)) → new_gcd0Gcd'15(Succ(vuv40), vuv41)
new_gcd0Gcd'10(vuv35, vuv36, Zero, Succ(vuv380)) → new_gcd0Gcd'12(Succ(vuv35), Pos(Succ(vuv36)))
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'13(vuv40, vuv41, Zero, Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'11(x0, Succ(x1)) → new_gcd0Gcd'1(new_primMinusNatS2(x0, x1), Succ(x1))
new_gcd0Gcd'1(Succ(Zero), Succ(vuv4000)) → new_gcd0Gcd'12(Zero, Pos(Succ(Succ(vuv4000))))
new_gcd0Gcd'0(Pos(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'0(Neg(Succ(Zero)), Succ(vuv4000)) → new_gcd0Gcd'15(Zero, Succ(vuv4000))
new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Zero) → new_gcd0Gcd'11(vuv35, vuv36)
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Zero) → new_gcd0Gcd'14(vuv6000, Zero)
new_gcd0Gcd'19(vuv72, vuv73) → new_gcd0Gcd'17(new_primMinusNatS2(Succ(vuv72), vuv73), vuv73, new_primMinusNatS2(Succ(vuv72), vuv73))
new_gcd0Gcd'14(vuv26, vuv27) → new_gcd0Gcd'16(new_primMinusNatS1(vuv26, vuv27), vuv27)
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Zero, vuv63) → new_gcd0Gcd'19(vuv6400, Zero)
new_gcd0Gcd'1(Succ(Succ(vuv6000)), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
The TRS R consists of the following rules:
new_primMinusNatS1(vuv23, Zero) → Succ(vuv23)
new_primMinusNatS1(vuv23, Succ(vuv240)) → new_primMinusNatS2(vuv23, vuv240)
new_primMinusNatS2(Succ(vuv230), Succ(vuv2400)) → new_primMinusNatS2(vuv230, vuv2400)
new_primMinusNatS2(Zero, Succ(vuv2400)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vuv230), Zero) → Succ(vuv230)
The set Q consists of the following terms:
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS1(x0, Succ(x1))
new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS1(x0, Zero)
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule new_gcd0Gcd'14(vuv26, vuv27) → new_gcd0Gcd'16(new_primMinusNatS1(vuv26, vuv27), vuv27) at position [0] we obtained the following new rules:
new_gcd0Gcd'14(x0, Succ(x1)) → new_gcd0Gcd'16(new_primMinusNatS2(x0, x1), Succ(x1))
new_gcd0Gcd'14(x0, Zero) → new_gcd0Gcd'16(Succ(x0), Zero)
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'18(vuv78, vuv79, Zero, Succ(vuv810)) → new_gcd0Gcd'12(Succ(vuv78), Neg(Succ(vuv79)))
new_gcd0Gcd'15(vuv29, vuv30) → new_gcd0Gcd'17(Succ(vuv30), vuv29, Succ(vuv30))
new_gcd0Gcd'14(x0, Zero) → new_gcd0Gcd'16(Succ(x0), Zero)
new_gcd0Gcd'16(Succ(Succ(vuv6000)), Zero) → new_gcd0Gcd'14(vuv6000, Zero)
new_gcd0Gcd'16(Succ(Zero), Succ(vuv4000)) → new_gcd0Gcd'15(Zero, Succ(vuv4000))
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810)
new_gcd0Gcd'16(Succ(Succ(vuv6000)), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'17(Succ(Zero), Succ(vuv620), vuv63) → new_gcd0Gcd'12(Zero, Neg(Succ(Succ(vuv620))))
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Succ(vuv620), vuv63) → new_gcd0Gcd'18(vuv6400, Succ(vuv620), vuv6400, vuv620)
new_gcd0Gcd'12(vuv400, vuv5) → new_gcd0Gcd'0(vuv5, vuv400)
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'18(vuv78, vuv79, Zero, Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'10(vuv35, vuv36, Zero, Zero) → new_gcd0Gcd'11(vuv35, vuv36)
new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Succ(vuv380)) → new_gcd0Gcd'10(vuv35, vuv36, vuv370, vuv380)
new_gcd0Gcd'0(Pos(Succ(Zero)), Succ(vuv4000)) → new_gcd0Gcd'12(Zero, Pos(Succ(Succ(vuv4000))))
new_gcd0Gcd'13(vuv40, vuv41, Zero, Succ(vuv430)) → new_gcd0Gcd'15(Succ(vuv40), vuv41)
new_gcd0Gcd'13(vuv40, vuv41, Zero, Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'10(vuv35, vuv36, Zero, Succ(vuv380)) → new_gcd0Gcd'12(Succ(vuv35), Pos(Succ(vuv36)))
new_gcd0Gcd'11(x0, Succ(x1)) → new_gcd0Gcd'1(new_primMinusNatS2(x0, x1), Succ(x1))
new_gcd0Gcd'1(Succ(Zero), Succ(vuv4000)) → new_gcd0Gcd'12(Zero, Pos(Succ(Succ(vuv4000))))
new_gcd0Gcd'0(Pos(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'14(x0, Succ(x1)) → new_gcd0Gcd'16(new_primMinusNatS2(x0, x1), Succ(x1))
new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Zero) → new_gcd0Gcd'11(vuv35, vuv36)
new_gcd0Gcd'0(Neg(Succ(Zero)), Succ(vuv4000)) → new_gcd0Gcd'15(Zero, Succ(vuv4000))
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Zero) → new_gcd0Gcd'14(vuv6000, Zero)
new_gcd0Gcd'19(vuv72, vuv73) → new_gcd0Gcd'17(new_primMinusNatS2(Succ(vuv72), vuv73), vuv73, new_primMinusNatS2(Succ(vuv72), vuv73))
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Zero, vuv63) → new_gcd0Gcd'19(vuv6400, Zero)
new_gcd0Gcd'1(Succ(Succ(vuv6000)), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
The TRS R consists of the following rules:
new_primMinusNatS1(vuv23, Zero) → Succ(vuv23)
new_primMinusNatS1(vuv23, Succ(vuv240)) → new_primMinusNatS2(vuv23, vuv240)
new_primMinusNatS2(Succ(vuv230), Succ(vuv2400)) → new_primMinusNatS2(vuv230, vuv2400)
new_primMinusNatS2(Zero, Succ(vuv2400)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vuv230), Zero) → Succ(vuv230)
The set Q consists of the following terms:
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS1(x0, Succ(x1))
new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS1(x0, Zero)
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 1 less node.
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'16(Succ(Succ(vuv6000)), Zero) → new_gcd0Gcd'14(vuv6000, Zero)
new_gcd0Gcd'14(x0, Zero) → new_gcd0Gcd'16(Succ(x0), Zero)
The TRS R consists of the following rules:
new_primMinusNatS1(vuv23, Zero) → Succ(vuv23)
new_primMinusNatS1(vuv23, Succ(vuv240)) → new_primMinusNatS2(vuv23, vuv240)
new_primMinusNatS2(Succ(vuv230), Succ(vuv2400)) → new_primMinusNatS2(vuv230, vuv2400)
new_primMinusNatS2(Zero, Succ(vuv2400)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vuv230), Zero) → Succ(vuv230)
The set Q consists of the following terms:
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS1(x0, Succ(x1))
new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS1(x0, Zero)
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'16(Succ(Succ(vuv6000)), Zero) → new_gcd0Gcd'14(vuv6000, Zero)
new_gcd0Gcd'14(x0, Zero) → new_gcd0Gcd'16(Succ(x0), Zero)
R is empty.
The set Q consists of the following terms:
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS1(x0, Succ(x1))
new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS1(x0, Zero)
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS1(x0, Succ(x1))
new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS1(x0, Zero)
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'14(x0, Zero) → new_gcd0Gcd'16(Succ(x0), Zero)
new_gcd0Gcd'16(Succ(Succ(vuv6000)), Zero) → new_gcd0Gcd'14(vuv6000, Zero)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:
new_gcd0Gcd'16(Succ(Succ(vuv6000)), Zero) → new_gcd0Gcd'14(vuv6000, Zero)
Used ordering: POLO with Polynomial interpretation [25]:
POL(Succ(x1)) = 1 + x1
POL(Zero) = 1
POL(new_gcd0Gcd'14(x1, x2)) = 2 + 2·x1 + 2·x2
POL(new_gcd0Gcd'16(x1, x2)) = 1 + 2·x1 + x2
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'14(x0, Zero) → new_gcd0Gcd'16(Succ(x0), Zero)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 1 less node.
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'18(vuv78, vuv79, Zero, Succ(vuv810)) → new_gcd0Gcd'12(Succ(vuv78), Neg(Succ(vuv79)))
new_gcd0Gcd'15(vuv29, vuv30) → new_gcd0Gcd'17(Succ(vuv30), vuv29, Succ(vuv30))
new_gcd0Gcd'16(Succ(Zero), Succ(vuv4000)) → new_gcd0Gcd'15(Zero, Succ(vuv4000))
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810)
new_gcd0Gcd'16(Succ(Succ(vuv6000)), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'17(Succ(Zero), Succ(vuv620), vuv63) → new_gcd0Gcd'12(Zero, Neg(Succ(Succ(vuv620))))
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Succ(vuv620), vuv63) → new_gcd0Gcd'18(vuv6400, Succ(vuv620), vuv6400, vuv620)
new_gcd0Gcd'12(vuv400, vuv5) → new_gcd0Gcd'0(vuv5, vuv400)
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'18(vuv78, vuv79, Zero, Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'10(vuv35, vuv36, Zero, Zero) → new_gcd0Gcd'11(vuv35, vuv36)
new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Succ(vuv380)) → new_gcd0Gcd'10(vuv35, vuv36, vuv370, vuv380)
new_gcd0Gcd'0(Pos(Succ(Zero)), Succ(vuv4000)) → new_gcd0Gcd'12(Zero, Pos(Succ(Succ(vuv4000))))
new_gcd0Gcd'13(vuv40, vuv41, Zero, Succ(vuv430)) → new_gcd0Gcd'15(Succ(vuv40), vuv41)
new_gcd0Gcd'13(vuv40, vuv41, Zero, Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'10(vuv35, vuv36, Zero, Succ(vuv380)) → new_gcd0Gcd'12(Succ(vuv35), Pos(Succ(vuv36)))
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'11(x0, Succ(x1)) → new_gcd0Gcd'1(new_primMinusNatS2(x0, x1), Succ(x1))
new_gcd0Gcd'1(Succ(Zero), Succ(vuv4000)) → new_gcd0Gcd'12(Zero, Pos(Succ(Succ(vuv4000))))
new_gcd0Gcd'0(Pos(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'14(x0, Succ(x1)) → new_gcd0Gcd'16(new_primMinusNatS2(x0, x1), Succ(x1))
new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Zero) → new_gcd0Gcd'11(vuv35, vuv36)
new_gcd0Gcd'0(Neg(Succ(Zero)), Succ(vuv4000)) → new_gcd0Gcd'15(Zero, Succ(vuv4000))
new_gcd0Gcd'19(vuv72, vuv73) → new_gcd0Gcd'17(new_primMinusNatS2(Succ(vuv72), vuv73), vuv73, new_primMinusNatS2(Succ(vuv72), vuv73))
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Zero, vuv63) → new_gcd0Gcd'19(vuv6400, Zero)
new_gcd0Gcd'1(Succ(Succ(vuv6000)), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
The TRS R consists of the following rules:
new_primMinusNatS1(vuv23, Zero) → Succ(vuv23)
new_primMinusNatS1(vuv23, Succ(vuv240)) → new_primMinusNatS2(vuv23, vuv240)
new_primMinusNatS2(Succ(vuv230), Succ(vuv2400)) → new_primMinusNatS2(vuv230, vuv2400)
new_primMinusNatS2(Zero, Succ(vuv2400)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vuv230), Zero) → Succ(vuv230)
The set Q consists of the following terms:
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS1(x0, Succ(x1))
new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS1(x0, Zero)
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'18(vuv78, vuv79, Zero, Succ(vuv810)) → new_gcd0Gcd'12(Succ(vuv78), Neg(Succ(vuv79)))
new_gcd0Gcd'15(vuv29, vuv30) → new_gcd0Gcd'17(Succ(vuv30), vuv29, Succ(vuv30))
new_gcd0Gcd'16(Succ(Zero), Succ(vuv4000)) → new_gcd0Gcd'15(Zero, Succ(vuv4000))
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810)
new_gcd0Gcd'16(Succ(Succ(vuv6000)), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'17(Succ(Zero), Succ(vuv620), vuv63) → new_gcd0Gcd'12(Zero, Neg(Succ(Succ(vuv620))))
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Succ(vuv620), vuv63) → new_gcd0Gcd'18(vuv6400, Succ(vuv620), vuv6400, vuv620)
new_gcd0Gcd'12(vuv400, vuv5) → new_gcd0Gcd'0(vuv5, vuv400)
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'18(vuv78, vuv79, Zero, Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'10(vuv35, vuv36, Zero, Zero) → new_gcd0Gcd'11(vuv35, vuv36)
new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Succ(vuv380)) → new_gcd0Gcd'10(vuv35, vuv36, vuv370, vuv380)
new_gcd0Gcd'0(Pos(Succ(Zero)), Succ(vuv4000)) → new_gcd0Gcd'12(Zero, Pos(Succ(Succ(vuv4000))))
new_gcd0Gcd'13(vuv40, vuv41, Zero, Succ(vuv430)) → new_gcd0Gcd'15(Succ(vuv40), vuv41)
new_gcd0Gcd'13(vuv40, vuv41, Zero, Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'10(vuv35, vuv36, Zero, Succ(vuv380)) → new_gcd0Gcd'12(Succ(vuv35), Pos(Succ(vuv36)))
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'11(x0, Succ(x1)) → new_gcd0Gcd'1(new_primMinusNatS2(x0, x1), Succ(x1))
new_gcd0Gcd'1(Succ(Zero), Succ(vuv4000)) → new_gcd0Gcd'12(Zero, Pos(Succ(Succ(vuv4000))))
new_gcd0Gcd'0(Pos(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'14(x0, Succ(x1)) → new_gcd0Gcd'16(new_primMinusNatS2(x0, x1), Succ(x1))
new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Zero) → new_gcd0Gcd'11(vuv35, vuv36)
new_gcd0Gcd'0(Neg(Succ(Zero)), Succ(vuv4000)) → new_gcd0Gcd'15(Zero, Succ(vuv4000))
new_gcd0Gcd'19(vuv72, vuv73) → new_gcd0Gcd'17(new_primMinusNatS2(Succ(vuv72), vuv73), vuv73, new_primMinusNatS2(Succ(vuv72), vuv73))
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Zero, vuv63) → new_gcd0Gcd'19(vuv6400, Zero)
new_gcd0Gcd'1(Succ(Succ(vuv6000)), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
The TRS R consists of the following rules:
new_primMinusNatS2(Succ(vuv230), Succ(vuv2400)) → new_primMinusNatS2(vuv230, vuv2400)
new_primMinusNatS2(Zero, Succ(vuv2400)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vuv230), Zero) → Succ(vuv230)
The set Q consists of the following terms:
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS1(x0, Succ(x1))
new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Succ(x0))
new_primMinusNatS1(x0, Zero)
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
new_primMinusNatS1(x0, Succ(x1))
new_primMinusNatS1(x0, Zero)
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'18(vuv78, vuv79, Zero, Succ(vuv810)) → new_gcd0Gcd'12(Succ(vuv78), Neg(Succ(vuv79)))
new_gcd0Gcd'15(vuv29, vuv30) → new_gcd0Gcd'17(Succ(vuv30), vuv29, Succ(vuv30))
new_gcd0Gcd'16(Succ(Zero), Succ(vuv4000)) → new_gcd0Gcd'15(Zero, Succ(vuv4000))
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810)
new_gcd0Gcd'16(Succ(Succ(vuv6000)), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'17(Succ(Zero), Succ(vuv620), vuv63) → new_gcd0Gcd'12(Zero, Neg(Succ(Succ(vuv620))))
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Succ(vuv620), vuv63) → new_gcd0Gcd'18(vuv6400, Succ(vuv620), vuv6400, vuv620)
new_gcd0Gcd'12(vuv400, vuv5) → new_gcd0Gcd'0(vuv5, vuv400)
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'18(vuv78, vuv79, Zero, Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'10(vuv35, vuv36, Zero, Zero) → new_gcd0Gcd'11(vuv35, vuv36)
new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Succ(vuv380)) → new_gcd0Gcd'10(vuv35, vuv36, vuv370, vuv380)
new_gcd0Gcd'0(Pos(Succ(Zero)), Succ(vuv4000)) → new_gcd0Gcd'12(Zero, Pos(Succ(Succ(vuv4000))))
new_gcd0Gcd'13(vuv40, vuv41, Zero, Succ(vuv430)) → new_gcd0Gcd'15(Succ(vuv40), vuv41)
new_gcd0Gcd'13(vuv40, vuv41, Zero, Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'10(vuv35, vuv36, Zero, Succ(vuv380)) → new_gcd0Gcd'12(Succ(vuv35), Pos(Succ(vuv36)))
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'11(x0, Succ(x1)) → new_gcd0Gcd'1(new_primMinusNatS2(x0, x1), Succ(x1))
new_gcd0Gcd'1(Succ(Zero), Succ(vuv4000)) → new_gcd0Gcd'12(Zero, Pos(Succ(Succ(vuv4000))))
new_gcd0Gcd'0(Pos(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'14(x0, Succ(x1)) → new_gcd0Gcd'16(new_primMinusNatS2(x0, x1), Succ(x1))
new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Zero) → new_gcd0Gcd'11(vuv35, vuv36)
new_gcd0Gcd'0(Neg(Succ(Zero)), Succ(vuv4000)) → new_gcd0Gcd'15(Zero, Succ(vuv4000))
new_gcd0Gcd'19(vuv72, vuv73) → new_gcd0Gcd'17(new_primMinusNatS2(Succ(vuv72), vuv73), vuv73, new_primMinusNatS2(Succ(vuv72), vuv73))
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Zero, vuv63) → new_gcd0Gcd'19(vuv6400, Zero)
new_gcd0Gcd'1(Succ(Succ(vuv6000)), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
The TRS R consists of the following rules:
new_primMinusNatS2(Succ(vuv230), Succ(vuv2400)) → new_primMinusNatS2(vuv230, vuv2400)
new_primMinusNatS2(Zero, Succ(vuv2400)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vuv230), Zero) → Succ(vuv230)
The set Q consists of the following terms:
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Succ(x0))
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule new_gcd0Gcd'12(vuv400, vuv5) → new_gcd0Gcd'0(vuv5, vuv400) we obtained the following new rules:
new_gcd0Gcd'12(Succ(z0), Pos(Succ(z1))) → new_gcd0Gcd'0(Pos(Succ(z1)), Succ(z0))
new_gcd0Gcd'12(Zero, Neg(Succ(Succ(z0)))) → new_gcd0Gcd'0(Neg(Succ(Succ(z0))), Zero)
new_gcd0Gcd'12(Zero, Pos(Succ(Succ(z0)))) → new_gcd0Gcd'0(Pos(Succ(Succ(z0))), Zero)
new_gcd0Gcd'12(Succ(z0), Neg(Succ(z1))) → new_gcd0Gcd'0(Neg(Succ(z1)), Succ(z0))
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'18(vuv78, vuv79, Zero, Succ(vuv810)) → new_gcd0Gcd'12(Succ(vuv78), Neg(Succ(vuv79)))
new_gcd0Gcd'15(vuv29, vuv30) → new_gcd0Gcd'17(Succ(vuv30), vuv29, Succ(vuv30))
new_gcd0Gcd'12(Zero, Pos(Succ(Succ(z0)))) → new_gcd0Gcd'0(Pos(Succ(Succ(z0))), Zero)
new_gcd0Gcd'16(Succ(Zero), Succ(vuv4000)) → new_gcd0Gcd'15(Zero, Succ(vuv4000))
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810)
new_gcd0Gcd'16(Succ(Succ(vuv6000)), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'17(Succ(Zero), Succ(vuv620), vuv63) → new_gcd0Gcd'12(Zero, Neg(Succ(Succ(vuv620))))
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Succ(vuv620), vuv63) → new_gcd0Gcd'18(vuv6400, Succ(vuv620), vuv6400, vuv620)
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'18(vuv78, vuv79, Zero, Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'10(vuv35, vuv36, Zero, Zero) → new_gcd0Gcd'11(vuv35, vuv36)
new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Succ(vuv380)) → new_gcd0Gcd'10(vuv35, vuv36, vuv370, vuv380)
new_gcd0Gcd'12(Succ(z0), Pos(Succ(z1))) → new_gcd0Gcd'0(Pos(Succ(z1)), Succ(z0))
new_gcd0Gcd'0(Pos(Succ(Zero)), Succ(vuv4000)) → new_gcd0Gcd'12(Zero, Pos(Succ(Succ(vuv4000))))
new_gcd0Gcd'12(Zero, Neg(Succ(Succ(z0)))) → new_gcd0Gcd'0(Neg(Succ(Succ(z0))), Zero)
new_gcd0Gcd'13(vuv40, vuv41, Zero, Succ(vuv430)) → new_gcd0Gcd'15(Succ(vuv40), vuv41)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'10(vuv35, vuv36, Zero, Succ(vuv380)) → new_gcd0Gcd'12(Succ(vuv35), Pos(Succ(vuv36)))
new_gcd0Gcd'13(vuv40, vuv41, Zero, Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'11(x0, Succ(x1)) → new_gcd0Gcd'1(new_primMinusNatS2(x0, x1), Succ(x1))
new_gcd0Gcd'1(Succ(Zero), Succ(vuv4000)) → new_gcd0Gcd'12(Zero, Pos(Succ(Succ(vuv4000))))
new_gcd0Gcd'12(Succ(z0), Neg(Succ(z1))) → new_gcd0Gcd'0(Neg(Succ(z1)), Succ(z0))
new_gcd0Gcd'0(Pos(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'14(x0, Succ(x1)) → new_gcd0Gcd'16(new_primMinusNatS2(x0, x1), Succ(x1))
new_gcd0Gcd'0(Neg(Succ(Zero)), Succ(vuv4000)) → new_gcd0Gcd'15(Zero, Succ(vuv4000))
new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Zero) → new_gcd0Gcd'11(vuv35, vuv36)
new_gcd0Gcd'19(vuv72, vuv73) → new_gcd0Gcd'17(new_primMinusNatS2(Succ(vuv72), vuv73), vuv73, new_primMinusNatS2(Succ(vuv72), vuv73))
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Zero, vuv63) → new_gcd0Gcd'19(vuv6400, Zero)
new_gcd0Gcd'1(Succ(Succ(vuv6000)), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
The TRS R consists of the following rules:
new_primMinusNatS2(Succ(vuv230), Succ(vuv2400)) → new_primMinusNatS2(vuv230, vuv2400)
new_primMinusNatS2(Zero, Succ(vuv2400)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vuv230), Zero) → Succ(vuv230)
The set Q consists of the following terms:
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Succ(x0))
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 5 less nodes.
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Zero) → new_gcd0Gcd'11(vuv35, vuv36)
new_gcd0Gcd'12(Succ(z0), Pos(Succ(z1))) → new_gcd0Gcd'0(Pos(Succ(z1)), Succ(z0))
new_gcd0Gcd'10(vuv35, vuv36, Zero, Succ(vuv380)) → new_gcd0Gcd'12(Succ(vuv35), Pos(Succ(vuv36)))
new_gcd0Gcd'11(x0, Succ(x1)) → new_gcd0Gcd'1(new_primMinusNatS2(x0, x1), Succ(x1))
new_gcd0Gcd'10(vuv35, vuv36, Zero, Zero) → new_gcd0Gcd'11(vuv35, vuv36)
new_gcd0Gcd'0(Pos(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Succ(vuv380)) → new_gcd0Gcd'10(vuv35, vuv36, vuv370, vuv380)
new_gcd0Gcd'1(Succ(Succ(vuv6000)), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
The TRS R consists of the following rules:
new_primMinusNatS2(Succ(vuv230), Succ(vuv2400)) → new_primMinusNatS2(vuv230, vuv2400)
new_primMinusNatS2(Zero, Succ(vuv2400)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vuv230), Zero) → Succ(vuv230)
The set Q consists of the following terms:
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Succ(x0))
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].
The following pairs can be oriented strictly and are deleted.
new_gcd0Gcd'1(Succ(Succ(vuv6000)), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
The remaining pairs can at least be oriented weakly.
new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Zero) → new_gcd0Gcd'11(vuv35, vuv36)
new_gcd0Gcd'12(Succ(z0), Pos(Succ(z1))) → new_gcd0Gcd'0(Pos(Succ(z1)), Succ(z0))
new_gcd0Gcd'10(vuv35, vuv36, Zero, Succ(vuv380)) → new_gcd0Gcd'12(Succ(vuv35), Pos(Succ(vuv36)))
new_gcd0Gcd'11(x0, Succ(x1)) → new_gcd0Gcd'1(new_primMinusNatS2(x0, x1), Succ(x1))
new_gcd0Gcd'10(vuv35, vuv36, Zero, Zero) → new_gcd0Gcd'11(vuv35, vuv36)
new_gcd0Gcd'0(Pos(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Succ(vuv380)) → new_gcd0Gcd'10(vuv35, vuv36, vuv370, vuv380)
Used ordering: Matrix interpretation [3]:
Non-tuple symbols:
M( new_primMinusNatS2(x1, x2) ) = | | + | | · | x1 | + | | · | x2 |
Tuple symbols:
M( new_gcd0Gcd'0(x1, x2) ) = | 0 | + | | · | x1 | + | | · | x2 |
M( new_gcd0Gcd'10(x1, ..., x4) ) = | 0 | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
M( new_gcd0Gcd'11(x1, x2) ) = | 0 | + | | · | x1 | + | | · | x2 |
M( new_gcd0Gcd'1(x1, x2) ) = | 0 | + | | · | x1 | + | | · | x2 |
M( new_gcd0Gcd'12(x1, x2) ) = | 0 | + | | · | x1 | + | | · | x2 |
Matrix type:
We used a basic matrix type which is not further parametrizeable.
As matrix orders are CE-compatible, we used usable rules w.r.t. argument filtering in the order.
The following usable rules [17] were oriented:
new_primMinusNatS2(Zero, Succ(vuv2400)) → Zero
new_primMinusNatS2(Succ(vuv230), Succ(vuv2400)) → new_primMinusNatS2(vuv230, vuv2400)
new_primMinusNatS2(Succ(vuv230), Zero) → Succ(vuv230)
new_primMinusNatS2(Zero, Zero) → Zero
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'12(Succ(z0), Pos(Succ(z1))) → new_gcd0Gcd'0(Pos(Succ(z1)), Succ(z0))
new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Zero) → new_gcd0Gcd'11(vuv35, vuv36)
new_gcd0Gcd'10(vuv35, vuv36, Zero, Succ(vuv380)) → new_gcd0Gcd'12(Succ(vuv35), Pos(Succ(vuv36)))
new_gcd0Gcd'11(x0, Succ(x1)) → new_gcd0Gcd'1(new_primMinusNatS2(x0, x1), Succ(x1))
new_gcd0Gcd'10(vuv35, vuv36, Zero, Zero) → new_gcd0Gcd'11(vuv35, vuv36)
new_gcd0Gcd'0(Pos(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Succ(vuv380)) → new_gcd0Gcd'10(vuv35, vuv36, vuv370, vuv380)
The TRS R consists of the following rules:
new_primMinusNatS2(Succ(vuv230), Succ(vuv2400)) → new_primMinusNatS2(vuv230, vuv2400)
new_primMinusNatS2(Zero, Succ(vuv2400)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vuv230), Zero) → Succ(vuv230)
The set Q consists of the following terms:
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Succ(x0))
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 3 less nodes.
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'12(Succ(z0), Pos(Succ(z1))) → new_gcd0Gcd'0(Pos(Succ(z1)), Succ(z0))
new_gcd0Gcd'10(vuv35, vuv36, Zero, Succ(vuv380)) → new_gcd0Gcd'12(Succ(vuv35), Pos(Succ(vuv36)))
new_gcd0Gcd'0(Pos(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Succ(vuv380)) → new_gcd0Gcd'10(vuv35, vuv36, vuv370, vuv380)
The TRS R consists of the following rules:
new_primMinusNatS2(Succ(vuv230), Succ(vuv2400)) → new_primMinusNatS2(vuv230, vuv2400)
new_primMinusNatS2(Zero, Succ(vuv2400)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vuv230), Zero) → Succ(vuv230)
The set Q consists of the following terms:
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Succ(x0))
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'12(Succ(z0), Pos(Succ(z1))) → new_gcd0Gcd'0(Pos(Succ(z1)), Succ(z0))
new_gcd0Gcd'10(vuv35, vuv36, Zero, Succ(vuv380)) → new_gcd0Gcd'12(Succ(vuv35), Pos(Succ(vuv36)))
new_gcd0Gcd'0(Pos(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Succ(vuv380)) → new_gcd0Gcd'10(vuv35, vuv36, vuv370, vuv380)
R is empty.
The set Q consists of the following terms:
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Succ(x0))
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Succ(x0))
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ NonInfProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'12(Succ(z0), Pos(Succ(z1))) → new_gcd0Gcd'0(Pos(Succ(z1)), Succ(z0))
new_gcd0Gcd'10(vuv35, vuv36, Zero, Succ(vuv380)) → new_gcd0Gcd'12(Succ(vuv35), Pos(Succ(vuv36)))
new_gcd0Gcd'0(Pos(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Succ(vuv380)) → new_gcd0Gcd'10(vuv35, vuv36, vuv370, vuv380)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The DP Problem is simplified using the Induction Calculus [18] with the following steps:
Note that final constraints are written in bold face.
For Pair new_gcd0Gcd'12(Succ(z0), Pos(Succ(z1))) → new_gcd0Gcd'0(Pos(Succ(z1)), Succ(z0)) the following chains were created:
- We consider the chain new_gcd0Gcd'10(vuv35, vuv36, Zero, Succ(vuv380)) → new_gcd0Gcd'12(Succ(vuv35), Pos(Succ(vuv36))), new_gcd0Gcd'12(Succ(z0), Pos(Succ(z1))) → new_gcd0Gcd'0(Pos(Succ(z1)), Succ(z0)) which results in the following constraint:
(1) (new_gcd0Gcd'12(Succ(x2), Pos(Succ(x3)))=new_gcd0Gcd'12(Succ(x5), Pos(Succ(x6))) ⇒ new_gcd0Gcd'12(Succ(x5), Pos(Succ(x6)))≥new_gcd0Gcd'0(Pos(Succ(x6)), Succ(x5)))
We simplified constraint (1) using rules (I), (II), (III) which results in the following new constraint:
(2) (new_gcd0Gcd'12(Succ(x2), Pos(Succ(x3)))≥new_gcd0Gcd'0(Pos(Succ(x3)), Succ(x2)))
For Pair new_gcd0Gcd'10(vuv35, vuv36, Zero, Succ(vuv380)) → new_gcd0Gcd'12(Succ(vuv35), Pos(Succ(vuv36))) the following chains were created:
- We consider the chain new_gcd0Gcd'0(Pos(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000), new_gcd0Gcd'10(vuv35, vuv36, Zero, Succ(vuv380)) → new_gcd0Gcd'12(Succ(vuv35), Pos(Succ(vuv36))) which results in the following constraint:
(3) (new_gcd0Gcd'10(x18, Succ(x19), x18, x19)=new_gcd0Gcd'10(x20, x21, Zero, Succ(x22)) ⇒ new_gcd0Gcd'10(x20, x21, Zero, Succ(x22))≥new_gcd0Gcd'12(Succ(x20), Pos(Succ(x21))))
We simplified constraint (3) using rules (I), (II), (III) which results in the following new constraint:
(4) (new_gcd0Gcd'10(Zero, Succ(Succ(x22)), Zero, Succ(x22))≥new_gcd0Gcd'12(Succ(Zero), Pos(Succ(Succ(Succ(x22))))))
- We consider the chain new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Succ(vuv380)) → new_gcd0Gcd'10(vuv35, vuv36, vuv370, vuv380), new_gcd0Gcd'10(vuv35, vuv36, Zero, Succ(vuv380)) → new_gcd0Gcd'12(Succ(vuv35), Pos(Succ(vuv36))) which results in the following constraint:
(5) (new_gcd0Gcd'10(x23, x24, x25, x26)=new_gcd0Gcd'10(x27, x28, Zero, Succ(x29)) ⇒ new_gcd0Gcd'10(x27, x28, Zero, Succ(x29))≥new_gcd0Gcd'12(Succ(x27), Pos(Succ(x28))))
We simplified constraint (5) using rules (I), (II), (III) which results in the following new constraint:
(6) (new_gcd0Gcd'10(x23, x24, Zero, Succ(x29))≥new_gcd0Gcd'12(Succ(x23), Pos(Succ(x24))))
For Pair new_gcd0Gcd'0(Pos(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000) the following chains were created:
- We consider the chain new_gcd0Gcd'12(Succ(z0), Pos(Succ(z1))) → new_gcd0Gcd'0(Pos(Succ(z1)), Succ(z0)), new_gcd0Gcd'0(Pos(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000) which results in the following constraint:
(7) (new_gcd0Gcd'0(Pos(Succ(x31)), Succ(x30))=new_gcd0Gcd'0(Pos(Succ(Succ(x32))), Succ(x33)) ⇒ new_gcd0Gcd'0(Pos(Succ(Succ(x32))), Succ(x33))≥new_gcd0Gcd'10(x32, Succ(x33), x32, x33))
We simplified constraint (7) using rules (I), (II), (III) which results in the following new constraint:
(8) (new_gcd0Gcd'0(Pos(Succ(Succ(x32))), Succ(x30))≥new_gcd0Gcd'10(x32, Succ(x30), x32, x30))
For Pair new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Succ(vuv380)) → new_gcd0Gcd'10(vuv35, vuv36, vuv370, vuv380) the following chains were created:
- We consider the chain new_gcd0Gcd'0(Pos(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000), new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Succ(vuv380)) → new_gcd0Gcd'10(vuv35, vuv36, vuv370, vuv380) which results in the following constraint:
(9) (new_gcd0Gcd'10(x48, Succ(x49), x48, x49)=new_gcd0Gcd'10(x50, x51, Succ(x52), Succ(x53)) ⇒ new_gcd0Gcd'10(x50, x51, Succ(x52), Succ(x53))≥new_gcd0Gcd'10(x50, x51, x52, x53))
We simplified constraint (9) using rules (I), (II), (III) which results in the following new constraint:
(10) (new_gcd0Gcd'10(Succ(x52), Succ(Succ(x53)), Succ(x52), Succ(x53))≥new_gcd0Gcd'10(Succ(x52), Succ(Succ(x53)), x52, x53))
- We consider the chain new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Succ(vuv380)) → new_gcd0Gcd'10(vuv35, vuv36, vuv370, vuv380), new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Succ(vuv380)) → new_gcd0Gcd'10(vuv35, vuv36, vuv370, vuv380) which results in the following constraint:
(11) (new_gcd0Gcd'10(x54, x55, x56, x57)=new_gcd0Gcd'10(x58, x59, Succ(x60), Succ(x61)) ⇒ new_gcd0Gcd'10(x58, x59, Succ(x60), Succ(x61))≥new_gcd0Gcd'10(x58, x59, x60, x61))
We simplified constraint (11) using rules (I), (II), (III) which results in the following new constraint:
(12) (new_gcd0Gcd'10(x54, x55, Succ(x60), Succ(x61))≥new_gcd0Gcd'10(x54, x55, x60, x61))
To summarize, we get the following constraints P≥ for the following pairs.
- new_gcd0Gcd'12(Succ(z0), Pos(Succ(z1))) → new_gcd0Gcd'0(Pos(Succ(z1)), Succ(z0))
- (new_gcd0Gcd'12(Succ(x2), Pos(Succ(x3)))≥new_gcd0Gcd'0(Pos(Succ(x3)), Succ(x2)))
- new_gcd0Gcd'10(vuv35, vuv36, Zero, Succ(vuv380)) → new_gcd0Gcd'12(Succ(vuv35), Pos(Succ(vuv36)))
- (new_gcd0Gcd'10(Zero, Succ(Succ(x22)), Zero, Succ(x22))≥new_gcd0Gcd'12(Succ(Zero), Pos(Succ(Succ(Succ(x22))))))
- (new_gcd0Gcd'10(x23, x24, Zero, Succ(x29))≥new_gcd0Gcd'12(Succ(x23), Pos(Succ(x24))))
- new_gcd0Gcd'0(Pos(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
- (new_gcd0Gcd'0(Pos(Succ(Succ(x32))), Succ(x30))≥new_gcd0Gcd'10(x32, Succ(x30), x32, x30))
- new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Succ(vuv380)) → new_gcd0Gcd'10(vuv35, vuv36, vuv370, vuv380)
- (new_gcd0Gcd'10(Succ(x52), Succ(Succ(x53)), Succ(x52), Succ(x53))≥new_gcd0Gcd'10(Succ(x52), Succ(Succ(x53)), x52, x53))
- (new_gcd0Gcd'10(x54, x55, Succ(x60), Succ(x61))≥new_gcd0Gcd'10(x54, x55, x60, x61))
The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation [18]:
POL(Pos(x1)) = 0
POL(Succ(x1)) = 1 + x1
POL(Zero) = 0
POL(c) = -1
POL(new_gcd0Gcd'0(x1, x2)) = 1 - x1 + x2
POL(new_gcd0Gcd'10(x1, x2, x3, x4)) = 1 + x1 - x3 + x4
POL(new_gcd0Gcd'12(x1, x2)) = 1 + x1 - x2
The following pairs are in P>:
new_gcd0Gcd'0(Pos(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
The following pairs are in Pbound:
new_gcd0Gcd'12(Succ(z0), Pos(Succ(z1))) → new_gcd0Gcd'0(Pos(Succ(z1)), Succ(z0))
new_gcd0Gcd'10(vuv35, vuv36, Zero, Succ(vuv380)) → new_gcd0Gcd'12(Succ(vuv35), Pos(Succ(vuv36)))
new_gcd0Gcd'0(Pos(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'10(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
There are no usable rules
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ NonInfProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'12(Succ(z0), Pos(Succ(z1))) → new_gcd0Gcd'0(Pos(Succ(z1)), Succ(z0))
new_gcd0Gcd'10(vuv35, vuv36, Zero, Succ(vuv380)) → new_gcd0Gcd'12(Succ(vuv35), Pos(Succ(vuv36)))
new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Succ(vuv380)) → new_gcd0Gcd'10(vuv35, vuv36, vuv370, vuv380)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 2 less nodes.
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ NonInfProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Succ(vuv380)) → new_gcd0Gcd'10(vuv35, vuv36, vuv370, vuv380)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_gcd0Gcd'10(vuv35, vuv36, Succ(vuv370), Succ(vuv380)) → new_gcd0Gcd'10(vuv35, vuv36, vuv370, vuv380)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'18(vuv78, vuv79, Zero, Succ(vuv810)) → new_gcd0Gcd'12(Succ(vuv78), Neg(Succ(vuv79)))
new_gcd0Gcd'13(vuv40, vuv41, Zero, Succ(vuv430)) → new_gcd0Gcd'15(Succ(vuv40), vuv41)
new_gcd0Gcd'13(vuv40, vuv41, Zero, Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'15(vuv29, vuv30) → new_gcd0Gcd'17(Succ(vuv30), vuv29, Succ(vuv30))
new_gcd0Gcd'12(Succ(z0), Neg(Succ(z1))) → new_gcd0Gcd'0(Neg(Succ(z1)), Succ(z0))
new_gcd0Gcd'16(Succ(Zero), Succ(vuv4000)) → new_gcd0Gcd'15(Zero, Succ(vuv4000))
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810)
new_gcd0Gcd'16(Succ(Succ(vuv6000)), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'14(x0, Succ(x1)) → new_gcd0Gcd'16(new_primMinusNatS2(x0, x1), Succ(x1))
new_gcd0Gcd'0(Neg(Succ(Zero)), Succ(vuv4000)) → new_gcd0Gcd'15(Zero, Succ(vuv4000))
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Succ(vuv620), vuv63) → new_gcd0Gcd'18(vuv6400, Succ(vuv620), vuv6400, vuv620)
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'19(vuv72, vuv73) → new_gcd0Gcd'17(new_primMinusNatS2(Succ(vuv72), vuv73), vuv73, new_primMinusNatS2(Succ(vuv72), vuv73))
new_gcd0Gcd'18(vuv78, vuv79, Zero, Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Zero, vuv63) → new_gcd0Gcd'19(vuv6400, Zero)
The TRS R consists of the following rules:
new_primMinusNatS2(Succ(vuv230), Succ(vuv2400)) → new_primMinusNatS2(vuv230, vuv2400)
new_primMinusNatS2(Zero, Succ(vuv2400)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vuv230), Zero) → Succ(vuv230)
The set Q consists of the following terms:
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Succ(x0))
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].
The following pairs can be oriented strictly and are deleted.
new_gcd0Gcd'0(Neg(Succ(Zero)), Succ(vuv4000)) → new_gcd0Gcd'15(Zero, Succ(vuv4000))
The remaining pairs can at least be oriented weakly.
new_gcd0Gcd'18(vuv78, vuv79, Zero, Succ(vuv810)) → new_gcd0Gcd'12(Succ(vuv78), Neg(Succ(vuv79)))
new_gcd0Gcd'13(vuv40, vuv41, Zero, Succ(vuv430)) → new_gcd0Gcd'15(Succ(vuv40), vuv41)
new_gcd0Gcd'13(vuv40, vuv41, Zero, Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'15(vuv29, vuv30) → new_gcd0Gcd'17(Succ(vuv30), vuv29, Succ(vuv30))
new_gcd0Gcd'12(Succ(z0), Neg(Succ(z1))) → new_gcd0Gcd'0(Neg(Succ(z1)), Succ(z0))
new_gcd0Gcd'16(Succ(Zero), Succ(vuv4000)) → new_gcd0Gcd'15(Zero, Succ(vuv4000))
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810)
new_gcd0Gcd'16(Succ(Succ(vuv6000)), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'14(x0, Succ(x1)) → new_gcd0Gcd'16(new_primMinusNatS2(x0, x1), Succ(x1))
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Succ(vuv620), vuv63) → new_gcd0Gcd'18(vuv6400, Succ(vuv620), vuv6400, vuv620)
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'19(vuv72, vuv73) → new_gcd0Gcd'17(new_primMinusNatS2(Succ(vuv72), vuv73), vuv73, new_primMinusNatS2(Succ(vuv72), vuv73))
new_gcd0Gcd'18(vuv78, vuv79, Zero, Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Zero, vuv63) → new_gcd0Gcd'19(vuv6400, Zero)
Used ordering: Matrix interpretation [3]:
Non-tuple symbols:
M( new_primMinusNatS2(x1, x2) ) = | | + | | · | x1 | + | | · | x2 |
Tuple symbols:
M( new_gcd0Gcd'0(x1, x2) ) = | 0 | + | | · | x1 | + | | · | x2 |
M( new_gcd0Gcd'16(x1, x2) ) = | 0 | + | | · | x1 | + | | · | x2 |
M( new_gcd0Gcd'18(x1, ..., x4) ) = | 0 | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
M( new_gcd0Gcd'13(x1, ..., x4) ) = | 0 | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
M( new_gcd0Gcd'12(x1, x2) ) = | 0 | + | | · | x1 | + | | · | x2 |
M( new_gcd0Gcd'15(x1, x2) ) = | 0 | + | | · | x1 | + | | · | x2 |
M( new_gcd0Gcd'19(x1, x2) ) = | 0 | + | | · | x1 | + | | · | x2 |
M( new_gcd0Gcd'14(x1, x2) ) = | 0 | + | | · | x1 | + | | · | x2 |
M( new_gcd0Gcd'17(x1, ..., x3) ) = | 0 | + | | · | x1 | + | | · | x2 | + | | · | x3 |
Matrix type:
We used a basic matrix type which is not further parametrizeable.
As matrix orders are CE-compatible, we used usable rules w.r.t. argument filtering in the order.
The following usable rules [17] were oriented:
none
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'18(vuv78, vuv79, Zero, Succ(vuv810)) → new_gcd0Gcd'12(Succ(vuv78), Neg(Succ(vuv79)))
new_gcd0Gcd'13(vuv40, vuv41, Zero, Succ(vuv430)) → new_gcd0Gcd'15(Succ(vuv40), vuv41)
new_gcd0Gcd'13(vuv40, vuv41, Zero, Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'15(vuv29, vuv30) → new_gcd0Gcd'17(Succ(vuv30), vuv29, Succ(vuv30))
new_gcd0Gcd'12(Succ(z0), Neg(Succ(z1))) → new_gcd0Gcd'0(Neg(Succ(z1)), Succ(z0))
new_gcd0Gcd'16(Succ(Zero), Succ(vuv4000)) → new_gcd0Gcd'15(Zero, Succ(vuv4000))
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810)
new_gcd0Gcd'16(Succ(Succ(vuv6000)), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'14(x0, Succ(x1)) → new_gcd0Gcd'16(new_primMinusNatS2(x0, x1), Succ(x1))
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Succ(vuv620), vuv63) → new_gcd0Gcd'18(vuv6400, Succ(vuv620), vuv6400, vuv620)
new_gcd0Gcd'19(vuv72, vuv73) → new_gcd0Gcd'17(new_primMinusNatS2(Succ(vuv72), vuv73), vuv73, new_primMinusNatS2(Succ(vuv72), vuv73))
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'18(vuv78, vuv79, Zero, Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Zero, vuv63) → new_gcd0Gcd'19(vuv6400, Zero)
The TRS R consists of the following rules:
new_primMinusNatS2(Succ(vuv230), Succ(vuv2400)) → new_primMinusNatS2(vuv230, vuv2400)
new_primMinusNatS2(Zero, Succ(vuv2400)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vuv230), Zero) → Succ(vuv230)
The set Q consists of the following terms:
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Succ(x0))
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].
The following pairs can be oriented strictly and are deleted.
new_gcd0Gcd'16(Succ(Zero), Succ(vuv4000)) → new_gcd0Gcd'15(Zero, Succ(vuv4000))
The remaining pairs can at least be oriented weakly.
new_gcd0Gcd'18(vuv78, vuv79, Zero, Succ(vuv810)) → new_gcd0Gcd'12(Succ(vuv78), Neg(Succ(vuv79)))
new_gcd0Gcd'13(vuv40, vuv41, Zero, Succ(vuv430)) → new_gcd0Gcd'15(Succ(vuv40), vuv41)
new_gcd0Gcd'13(vuv40, vuv41, Zero, Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'15(vuv29, vuv30) → new_gcd0Gcd'17(Succ(vuv30), vuv29, Succ(vuv30))
new_gcd0Gcd'12(Succ(z0), Neg(Succ(z1))) → new_gcd0Gcd'0(Neg(Succ(z1)), Succ(z0))
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810)
new_gcd0Gcd'16(Succ(Succ(vuv6000)), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'14(x0, Succ(x1)) → new_gcd0Gcd'16(new_primMinusNatS2(x0, x1), Succ(x1))
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Succ(vuv620), vuv63) → new_gcd0Gcd'18(vuv6400, Succ(vuv620), vuv6400, vuv620)
new_gcd0Gcd'19(vuv72, vuv73) → new_gcd0Gcd'17(new_primMinusNatS2(Succ(vuv72), vuv73), vuv73, new_primMinusNatS2(Succ(vuv72), vuv73))
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'18(vuv78, vuv79, Zero, Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Zero, vuv63) → new_gcd0Gcd'19(vuv6400, Zero)
Used ordering: Matrix interpretation [3]:
Non-tuple symbols:
M( new_primMinusNatS2(x1, x2) ) = | | + | | · | x1 | + | | · | x2 |
Tuple symbols:
M( new_gcd0Gcd'0(x1, x2) ) = | 0 | + | | · | x1 | + | | · | x2 |
M( new_gcd0Gcd'16(x1, x2) ) = | 0 | + | | · | x1 | + | | · | x2 |
M( new_gcd0Gcd'18(x1, ..., x4) ) = | 0 | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
M( new_gcd0Gcd'13(x1, ..., x4) ) = | 0 | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
M( new_gcd0Gcd'12(x1, x2) ) = | 0 | + | | · | x1 | + | | · | x2 |
M( new_gcd0Gcd'15(x1, x2) ) = | 0 | + | | · | x1 | + | | · | x2 |
M( new_gcd0Gcd'19(x1, x2) ) = | 0 | + | | · | x1 | + | | · | x2 |
M( new_gcd0Gcd'14(x1, x2) ) = | 0 | + | | · | x1 | + | | · | x2 |
M( new_gcd0Gcd'17(x1, ..., x3) ) = | 0 | + | | · | x1 | + | | · | x2 | + | | · | x3 |
Matrix type:
We used a basic matrix type which is not further parametrizeable.
As matrix orders are CE-compatible, we used usable rules w.r.t. argument filtering in the order.
The following usable rules [17] were oriented:
new_primMinusNatS2(Zero, Succ(vuv2400)) → Zero
new_primMinusNatS2(Succ(vuv230), Succ(vuv2400)) → new_primMinusNatS2(vuv230, vuv2400)
new_primMinusNatS2(Succ(vuv230), Zero) → Succ(vuv230)
new_primMinusNatS2(Zero, Zero) → Zero
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'18(vuv78, vuv79, Zero, Succ(vuv810)) → new_gcd0Gcd'12(Succ(vuv78), Neg(Succ(vuv79)))
new_gcd0Gcd'13(vuv40, vuv41, Zero, Succ(vuv430)) → new_gcd0Gcd'15(Succ(vuv40), vuv41)
new_gcd0Gcd'13(vuv40, vuv41, Zero, Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'15(vuv29, vuv30) → new_gcd0Gcd'17(Succ(vuv30), vuv29, Succ(vuv30))
new_gcd0Gcd'12(Succ(z0), Neg(Succ(z1))) → new_gcd0Gcd'0(Neg(Succ(z1)), Succ(z0))
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810)
new_gcd0Gcd'16(Succ(Succ(vuv6000)), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'14(x0, Succ(x1)) → new_gcd0Gcd'16(new_primMinusNatS2(x0, x1), Succ(x1))
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Succ(vuv620), vuv63) → new_gcd0Gcd'18(vuv6400, Succ(vuv620), vuv6400, vuv620)
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'19(vuv72, vuv73) → new_gcd0Gcd'17(new_primMinusNatS2(Succ(vuv72), vuv73), vuv73, new_primMinusNatS2(Succ(vuv72), vuv73))
new_gcd0Gcd'18(vuv78, vuv79, Zero, Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Zero, vuv63) → new_gcd0Gcd'19(vuv6400, Zero)
The TRS R consists of the following rules:
new_primMinusNatS2(Succ(vuv230), Succ(vuv2400)) → new_primMinusNatS2(vuv230, vuv2400)
new_primMinusNatS2(Zero, Succ(vuv2400)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vuv230), Zero) → Succ(vuv230)
The set Q consists of the following terms:
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Succ(x0))
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].
The following pairs can be oriented strictly and are deleted.
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Zero, vuv63) → new_gcd0Gcd'19(vuv6400, Zero)
The remaining pairs can at least be oriented weakly.
new_gcd0Gcd'18(vuv78, vuv79, Zero, Succ(vuv810)) → new_gcd0Gcd'12(Succ(vuv78), Neg(Succ(vuv79)))
new_gcd0Gcd'13(vuv40, vuv41, Zero, Succ(vuv430)) → new_gcd0Gcd'15(Succ(vuv40), vuv41)
new_gcd0Gcd'13(vuv40, vuv41, Zero, Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'15(vuv29, vuv30) → new_gcd0Gcd'17(Succ(vuv30), vuv29, Succ(vuv30))
new_gcd0Gcd'12(Succ(z0), Neg(Succ(z1))) → new_gcd0Gcd'0(Neg(Succ(z1)), Succ(z0))
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810)
new_gcd0Gcd'16(Succ(Succ(vuv6000)), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'14(x0, Succ(x1)) → new_gcd0Gcd'16(new_primMinusNatS2(x0, x1), Succ(x1))
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Succ(vuv620), vuv63) → new_gcd0Gcd'18(vuv6400, Succ(vuv620), vuv6400, vuv620)
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'19(vuv72, vuv73) → new_gcd0Gcd'17(new_primMinusNatS2(Succ(vuv72), vuv73), vuv73, new_primMinusNatS2(Succ(vuv72), vuv73))
new_gcd0Gcd'18(vuv78, vuv79, Zero, Zero) → new_gcd0Gcd'19(vuv78, vuv79)
Used ordering: Matrix interpretation [3]:
Non-tuple symbols:
M( new_primMinusNatS2(x1, x2) ) = | | + | | · | x1 | + | | · | x2 |
Tuple symbols:
M( new_gcd0Gcd'0(x1, x2) ) = | 0 | + | | · | x1 | + | | · | x2 |
M( new_gcd0Gcd'16(x1, x2) ) = | 0 | + | | · | x1 | + | | · | x2 |
M( new_gcd0Gcd'18(x1, ..., x4) ) = | 0 | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
M( new_gcd0Gcd'13(x1, ..., x4) ) = | 0 | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
M( new_gcd0Gcd'12(x1, x2) ) = | 0 | + | | · | x1 | + | | · | x2 |
M( new_gcd0Gcd'15(x1, x2) ) = | 0 | + | | · | x1 | + | | · | x2 |
M( new_gcd0Gcd'19(x1, x2) ) = | 0 | + | | · | x1 | + | | · | x2 |
M( new_gcd0Gcd'14(x1, x2) ) = | 0 | + | | · | x1 | + | | · | x2 |
M( new_gcd0Gcd'17(x1, ..., x3) ) = | 0 | + | | · | x1 | + | | · | x2 | + | | · | x3 |
Matrix type:
We used a basic matrix type which is not further parametrizeable.
As matrix orders are CE-compatible, we used usable rules w.r.t. argument filtering in the order.
The following usable rules [17] were oriented:
new_primMinusNatS2(Zero, Succ(vuv2400)) → Zero
new_primMinusNatS2(Succ(vuv230), Succ(vuv2400)) → new_primMinusNatS2(vuv230, vuv2400)
new_primMinusNatS2(Succ(vuv230), Zero) → Succ(vuv230)
new_primMinusNatS2(Zero, Zero) → Zero
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'18(vuv78, vuv79, Zero, Succ(vuv810)) → new_gcd0Gcd'12(Succ(vuv78), Neg(Succ(vuv79)))
new_gcd0Gcd'13(vuv40, vuv41, Zero, Succ(vuv430)) → new_gcd0Gcd'15(Succ(vuv40), vuv41)
new_gcd0Gcd'13(vuv40, vuv41, Zero, Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'15(vuv29, vuv30) → new_gcd0Gcd'17(Succ(vuv30), vuv29, Succ(vuv30))
new_gcd0Gcd'12(Succ(z0), Neg(Succ(z1))) → new_gcd0Gcd'0(Neg(Succ(z1)), Succ(z0))
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810)
new_gcd0Gcd'16(Succ(Succ(vuv6000)), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'14(x0, Succ(x1)) → new_gcd0Gcd'16(new_primMinusNatS2(x0, x1), Succ(x1))
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Succ(vuv620), vuv63) → new_gcd0Gcd'18(vuv6400, Succ(vuv620), vuv6400, vuv620)
new_gcd0Gcd'19(vuv72, vuv73) → new_gcd0Gcd'17(new_primMinusNatS2(Succ(vuv72), vuv73), vuv73, new_primMinusNatS2(Succ(vuv72), vuv73))
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'18(vuv78, vuv79, Zero, Zero) → new_gcd0Gcd'19(vuv78, vuv79)
The TRS R consists of the following rules:
new_primMinusNatS2(Succ(vuv230), Succ(vuv2400)) → new_primMinusNatS2(vuv230, vuv2400)
new_primMinusNatS2(Zero, Succ(vuv2400)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vuv230), Zero) → Succ(vuv230)
The set Q consists of the following terms:
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Succ(x0))
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].
The following pairs can be oriented strictly and are deleted.
new_gcd0Gcd'13(vuv40, vuv41, Zero, Zero) → new_gcd0Gcd'14(vuv40, vuv41)
new_gcd0Gcd'14(x0, Succ(x1)) → new_gcd0Gcd'16(new_primMinusNatS2(x0, x1), Succ(x1))
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Zero) → new_gcd0Gcd'14(vuv40, vuv41)
The remaining pairs can at least be oriented weakly.
new_gcd0Gcd'18(vuv78, vuv79, Zero, Succ(vuv810)) → new_gcd0Gcd'12(Succ(vuv78), Neg(Succ(vuv79)))
new_gcd0Gcd'13(vuv40, vuv41, Zero, Succ(vuv430)) → new_gcd0Gcd'15(Succ(vuv40), vuv41)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'15(vuv29, vuv30) → new_gcd0Gcd'17(Succ(vuv30), vuv29, Succ(vuv30))
new_gcd0Gcd'12(Succ(z0), Neg(Succ(z1))) → new_gcd0Gcd'0(Neg(Succ(z1)), Succ(z0))
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810)
new_gcd0Gcd'16(Succ(Succ(vuv6000)), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Succ(vuv620), vuv63) → new_gcd0Gcd'18(vuv6400, Succ(vuv620), vuv6400, vuv620)
new_gcd0Gcd'19(vuv72, vuv73) → new_gcd0Gcd'17(new_primMinusNatS2(Succ(vuv72), vuv73), vuv73, new_primMinusNatS2(Succ(vuv72), vuv73))
new_gcd0Gcd'18(vuv78, vuv79, Zero, Zero) → new_gcd0Gcd'19(vuv78, vuv79)
Used ordering: Matrix interpretation [3]:
Non-tuple symbols:
M( new_primMinusNatS2(x1, x2) ) = | | + | | · | x1 | + | | · | x2 |
Tuple symbols:
M( new_gcd0Gcd'0(x1, x2) ) = | 1 | + | | · | x1 | + | | · | x2 |
M( new_gcd0Gcd'16(x1, x2) ) = | 0 | + | | · | x1 | + | | · | x2 |
M( new_gcd0Gcd'18(x1, ..., x4) ) = | 1 | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
M( new_gcd0Gcd'13(x1, ..., x4) ) = | 1 | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
M( new_gcd0Gcd'12(x1, x2) ) = | 0 | + | | · | x1 | + | | · | x2 |
M( new_gcd0Gcd'15(x1, x2) ) = | 0 | + | | · | x1 | + | | · | x2 |
M( new_gcd0Gcd'19(x1, x2) ) = | 1 | + | | · | x1 | + | | · | x2 |
M( new_gcd0Gcd'14(x1, x2) ) = | 0 | + | | · | x1 | + | | · | x2 |
M( new_gcd0Gcd'17(x1, ..., x3) ) = | 0 | + | | · | x1 | + | | · | x2 | + | | · | x3 |
Matrix type:
We used a basic matrix type which is not further parametrizeable.
As matrix orders are CE-compatible, we used usable rules w.r.t. argument filtering in the order.
The following usable rules [17] were oriented:
new_primMinusNatS2(Zero, Succ(vuv2400)) → Zero
new_primMinusNatS2(Succ(vuv230), Succ(vuv2400)) → new_primMinusNatS2(vuv230, vuv2400)
new_primMinusNatS2(Succ(vuv230), Zero) → Succ(vuv230)
new_primMinusNatS2(Zero, Zero) → Zero
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'16(Succ(Succ(vuv6000)), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'18(vuv78, vuv79, Zero, Succ(vuv810)) → new_gcd0Gcd'12(Succ(vuv78), Neg(Succ(vuv79)))
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Succ(vuv620), vuv63) → new_gcd0Gcd'18(vuv6400, Succ(vuv620), vuv6400, vuv620)
new_gcd0Gcd'13(vuv40, vuv41, Zero, Succ(vuv430)) → new_gcd0Gcd'15(Succ(vuv40), vuv41)
new_gcd0Gcd'19(vuv72, vuv73) → new_gcd0Gcd'17(new_primMinusNatS2(Succ(vuv72), vuv73), vuv73, new_primMinusNatS2(Succ(vuv72), vuv73))
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'15(vuv29, vuv30) → new_gcd0Gcd'17(Succ(vuv30), vuv29, Succ(vuv30))
new_gcd0Gcd'18(vuv78, vuv79, Zero, Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'12(Succ(z0), Neg(Succ(z1))) → new_gcd0Gcd'0(Neg(Succ(z1)), Succ(z0))
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810)
The TRS R consists of the following rules:
new_primMinusNatS2(Succ(vuv230), Succ(vuv2400)) → new_primMinusNatS2(vuv230, vuv2400)
new_primMinusNatS2(Zero, Succ(vuv2400)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vuv230), Zero) → Succ(vuv230)
The set Q consists of the following terms:
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Succ(x0))
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'18(vuv78, vuv79, Zero, Succ(vuv810)) → new_gcd0Gcd'12(Succ(vuv78), Neg(Succ(vuv79)))
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Succ(vuv620), vuv63) → new_gcd0Gcd'18(vuv6400, Succ(vuv620), vuv6400, vuv620)
new_gcd0Gcd'13(vuv40, vuv41, Zero, Succ(vuv430)) → new_gcd0Gcd'15(Succ(vuv40), vuv41)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'19(vuv72, vuv73) → new_gcd0Gcd'17(new_primMinusNatS2(Succ(vuv72), vuv73), vuv73, new_primMinusNatS2(Succ(vuv72), vuv73))
new_gcd0Gcd'15(vuv29, vuv30) → new_gcd0Gcd'17(Succ(vuv30), vuv29, Succ(vuv30))
new_gcd0Gcd'18(vuv78, vuv79, Zero, Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'12(Succ(z0), Neg(Succ(z1))) → new_gcd0Gcd'0(Neg(Succ(z1)), Succ(z0))
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810)
The TRS R consists of the following rules:
new_primMinusNatS2(Succ(vuv230), Succ(vuv2400)) → new_primMinusNatS2(vuv230, vuv2400)
new_primMinusNatS2(Zero, Succ(vuv2400)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vuv230), Zero) → Succ(vuv230)
The set Q consists of the following terms:
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Succ(x0))
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].
The following pairs can be oriented strictly and are deleted.
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Zero) → new_gcd0Gcd'19(vuv78, vuv79)
new_gcd0Gcd'18(vuv78, vuv79, Zero, Zero) → new_gcd0Gcd'19(vuv78, vuv79)
The remaining pairs can at least be oriented weakly.
new_gcd0Gcd'18(vuv78, vuv79, Zero, Succ(vuv810)) → new_gcd0Gcd'12(Succ(vuv78), Neg(Succ(vuv79)))
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Succ(vuv620), vuv63) → new_gcd0Gcd'18(vuv6400, Succ(vuv620), vuv6400, vuv620)
new_gcd0Gcd'13(vuv40, vuv41, Zero, Succ(vuv430)) → new_gcd0Gcd'15(Succ(vuv40), vuv41)
new_gcd0Gcd'19(vuv72, vuv73) → new_gcd0Gcd'17(new_primMinusNatS2(Succ(vuv72), vuv73), vuv73, new_primMinusNatS2(Succ(vuv72), vuv73))
new_gcd0Gcd'15(vuv29, vuv30) → new_gcd0Gcd'17(Succ(vuv30), vuv29, Succ(vuv30))
new_gcd0Gcd'12(Succ(z0), Neg(Succ(z1))) → new_gcd0Gcd'0(Neg(Succ(z1)), Succ(z0))
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810)
Used ordering: Matrix interpretation [3]:
Non-tuple symbols:
M( new_primMinusNatS2(x1, x2) ) = | | + | | · | x1 | + | | · | x2 |
Tuple symbols:
M( new_gcd0Gcd'0(x1, x2) ) = | 1 | + | | · | x1 | + | | · | x2 |
M( new_gcd0Gcd'18(x1, ..., x4) ) = | 1 | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
M( new_gcd0Gcd'13(x1, ..., x4) ) = | 0 | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
M( new_gcd0Gcd'12(x1, x2) ) = | 1 | + | | · | x1 | + | | · | x2 |
M( new_gcd0Gcd'15(x1, x2) ) = | 0 | + | | · | x1 | + | | · | x2 |
M( new_gcd0Gcd'19(x1, x2) ) = | 0 | + | | · | x1 | + | | · | x2 |
M( new_gcd0Gcd'17(x1, ..., x3) ) = | 0 | + | | · | x1 | + | | · | x2 | + | | · | x3 |
Matrix type:
We used a basic matrix type which is not further parametrizeable.
As matrix orders are CE-compatible, we used usable rules w.r.t. argument filtering in the order.
The following usable rules [17] were oriented:
new_primMinusNatS2(Zero, Succ(vuv2400)) → Zero
new_primMinusNatS2(Succ(vuv230), Succ(vuv2400)) → new_primMinusNatS2(vuv230, vuv2400)
new_primMinusNatS2(Succ(vuv230), Zero) → Succ(vuv230)
new_primMinusNatS2(Zero, Zero) → Zero
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'18(vuv78, vuv79, Zero, Succ(vuv810)) → new_gcd0Gcd'12(Succ(vuv78), Neg(Succ(vuv79)))
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Succ(vuv620), vuv63) → new_gcd0Gcd'18(vuv6400, Succ(vuv620), vuv6400, vuv620)
new_gcd0Gcd'13(vuv40, vuv41, Zero, Succ(vuv430)) → new_gcd0Gcd'15(Succ(vuv40), vuv41)
new_gcd0Gcd'19(vuv72, vuv73) → new_gcd0Gcd'17(new_primMinusNatS2(Succ(vuv72), vuv73), vuv73, new_primMinusNatS2(Succ(vuv72), vuv73))
new_gcd0Gcd'15(vuv29, vuv30) → new_gcd0Gcd'17(Succ(vuv30), vuv29, Succ(vuv30))
new_gcd0Gcd'12(Succ(z0), Neg(Succ(z1))) → new_gcd0Gcd'0(Neg(Succ(z1)), Succ(z0))
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810)
The TRS R consists of the following rules:
new_primMinusNatS2(Succ(vuv230), Succ(vuv2400)) → new_primMinusNatS2(vuv230, vuv2400)
new_primMinusNatS2(Zero, Succ(vuv2400)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vuv230), Zero) → Succ(vuv230)
The set Q consists of the following terms:
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Succ(x0))
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'18(vuv78, vuv79, Zero, Succ(vuv810)) → new_gcd0Gcd'12(Succ(vuv78), Neg(Succ(vuv79)))
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Succ(vuv620), vuv63) → new_gcd0Gcd'18(vuv6400, Succ(vuv620), vuv6400, vuv620)
new_gcd0Gcd'13(vuv40, vuv41, Zero, Succ(vuv430)) → new_gcd0Gcd'15(Succ(vuv40), vuv41)
new_gcd0Gcd'15(vuv29, vuv30) → new_gcd0Gcd'17(Succ(vuv30), vuv29, Succ(vuv30))
new_gcd0Gcd'12(Succ(z0), Neg(Succ(z1))) → new_gcd0Gcd'0(Neg(Succ(z1)), Succ(z0))
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810)
The TRS R consists of the following rules:
new_primMinusNatS2(Succ(vuv230), Succ(vuv2400)) → new_primMinusNatS2(vuv230, vuv2400)
new_primMinusNatS2(Zero, Succ(vuv2400)) → Zero
new_primMinusNatS2(Zero, Zero) → Zero
new_primMinusNatS2(Succ(vuv230), Zero) → Succ(vuv230)
The set Q consists of the following terms:
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Succ(x0))
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'18(vuv78, vuv79, Zero, Succ(vuv810)) → new_gcd0Gcd'12(Succ(vuv78), Neg(Succ(vuv79)))
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Succ(vuv620), vuv63) → new_gcd0Gcd'18(vuv6400, Succ(vuv620), vuv6400, vuv620)
new_gcd0Gcd'13(vuv40, vuv41, Zero, Succ(vuv430)) → new_gcd0Gcd'15(Succ(vuv40), vuv41)
new_gcd0Gcd'15(vuv29, vuv30) → new_gcd0Gcd'17(Succ(vuv30), vuv29, Succ(vuv30))
new_gcd0Gcd'12(Succ(z0), Neg(Succ(z1))) → new_gcd0Gcd'0(Neg(Succ(z1)), Succ(z0))
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810)
R is empty.
The set Q consists of the following terms:
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Succ(x0))
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
new_primMinusNatS2(Zero, Zero)
new_primMinusNatS2(Succ(x0), Zero)
new_primMinusNatS2(Succ(x0), Succ(x1))
new_primMinusNatS2(Zero, Succ(x0))
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'18(vuv78, vuv79, Zero, Succ(vuv810)) → new_gcd0Gcd'12(Succ(vuv78), Neg(Succ(vuv79)))
new_gcd0Gcd'17(Succ(Succ(vuv6400)), Succ(vuv620), vuv63) → new_gcd0Gcd'18(vuv6400, Succ(vuv620), vuv6400, vuv620)
new_gcd0Gcd'13(vuv40, vuv41, Zero, Succ(vuv430)) → new_gcd0Gcd'15(Succ(vuv40), vuv41)
new_gcd0Gcd'15(vuv29, vuv30) → new_gcd0Gcd'17(Succ(vuv30), vuv29, Succ(vuv30))
new_gcd0Gcd'12(Succ(z0), Neg(Succ(z1))) → new_gcd0Gcd'0(Neg(Succ(z1)), Succ(z0))
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule new_gcd0Gcd'17(Succ(Succ(vuv6400)), Succ(vuv620), vuv63) → new_gcd0Gcd'18(vuv6400, Succ(vuv620), vuv6400, vuv620) we obtained the following new rules:
new_gcd0Gcd'17(Succ(Succ(x0)), Succ(x1), Succ(Succ(x0))) → new_gcd0Gcd'18(x0, Succ(x1), x0, x1)
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ NonInfProof
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'18(vuv78, vuv79, Zero, Succ(vuv810)) → new_gcd0Gcd'12(Succ(vuv78), Neg(Succ(vuv79)))
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'13(vuv40, vuv41, Zero, Succ(vuv430)) → new_gcd0Gcd'15(Succ(vuv40), vuv41)
new_gcd0Gcd'17(Succ(Succ(x0)), Succ(x1), Succ(Succ(x0))) → new_gcd0Gcd'18(x0, Succ(x1), x0, x1)
new_gcd0Gcd'15(vuv29, vuv30) → new_gcd0Gcd'17(Succ(vuv30), vuv29, Succ(vuv30))
new_gcd0Gcd'12(Succ(z0), Neg(Succ(z1))) → new_gcd0Gcd'0(Neg(Succ(z1)), Succ(z0))
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The DP Problem is simplified using the Induction Calculus [18] with the following steps:
Note that final constraints are written in bold face.
For Pair new_gcd0Gcd'18(vuv78, vuv79, Zero, Succ(vuv810)) → new_gcd0Gcd'12(Succ(vuv78), Neg(Succ(vuv79))) the following chains were created:
- We consider the chain new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810), new_gcd0Gcd'18(vuv78, vuv79, Zero, Succ(vuv810)) → new_gcd0Gcd'12(Succ(vuv78), Neg(Succ(vuv79))) which results in the following constraint:
(1) (new_gcd0Gcd'18(x16, x17, x18, x19)=new_gcd0Gcd'18(x20, x21, Zero, Succ(x22)) ⇒ new_gcd0Gcd'18(x20, x21, Zero, Succ(x22))≥new_gcd0Gcd'12(Succ(x20), Neg(Succ(x21))))
We simplified constraint (1) using rules (I), (II), (III) which results in the following new constraint:
(2) (new_gcd0Gcd'18(x16, x17, Zero, Succ(x22))≥new_gcd0Gcd'12(Succ(x16), Neg(Succ(x17))))
- We consider the chain new_gcd0Gcd'17(Succ(Succ(x0)), Succ(x1), Succ(Succ(x0))) → new_gcd0Gcd'18(x0, Succ(x1), x0, x1), new_gcd0Gcd'18(vuv78, vuv79, Zero, Succ(vuv810)) → new_gcd0Gcd'12(Succ(vuv78), Neg(Succ(vuv79))) which results in the following constraint:
(3) (new_gcd0Gcd'18(x23, Succ(x24), x23, x24)=new_gcd0Gcd'18(x25, x26, Zero, Succ(x27)) ⇒ new_gcd0Gcd'18(x25, x26, Zero, Succ(x27))≥new_gcd0Gcd'12(Succ(x25), Neg(Succ(x26))))
We simplified constraint (3) using rules (I), (II), (III) which results in the following new constraint:
(4) (new_gcd0Gcd'18(Zero, Succ(Succ(x27)), Zero, Succ(x27))≥new_gcd0Gcd'12(Succ(Zero), Neg(Succ(Succ(Succ(x27))))))
For Pair new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000) the following chains were created:
- We consider the chain new_gcd0Gcd'12(Succ(z0), Neg(Succ(z1))) → new_gcd0Gcd'0(Neg(Succ(z1)), Succ(z0)), new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000) which results in the following constraint:
(5) (new_gcd0Gcd'0(Neg(Succ(x39)), Succ(x38))=new_gcd0Gcd'0(Neg(Succ(Succ(x40))), Succ(x41)) ⇒ new_gcd0Gcd'0(Neg(Succ(Succ(x40))), Succ(x41))≥new_gcd0Gcd'13(x40, Succ(x41), x40, x41))
We simplified constraint (5) using rules (I), (II), (III) which results in the following new constraint:
(6) (new_gcd0Gcd'0(Neg(Succ(Succ(x40))), Succ(x38))≥new_gcd0Gcd'13(x40, Succ(x38), x40, x38))
For Pair new_gcd0Gcd'13(vuv40, vuv41, Zero, Succ(vuv430)) → new_gcd0Gcd'15(Succ(vuv40), vuv41) the following chains were created:
- We consider the chain new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000), new_gcd0Gcd'13(vuv40, vuv41, Zero, Succ(vuv430)) → new_gcd0Gcd'15(Succ(vuv40), vuv41) which results in the following constraint:
(7) (new_gcd0Gcd'13(x55, Succ(x56), x55, x56)=new_gcd0Gcd'13(x57, x58, Zero, Succ(x59)) ⇒ new_gcd0Gcd'13(x57, x58, Zero, Succ(x59))≥new_gcd0Gcd'15(Succ(x57), x58))
We simplified constraint (7) using rules (I), (II), (III) which results in the following new constraint:
(8) (new_gcd0Gcd'13(Zero, Succ(Succ(x59)), Zero, Succ(x59))≥new_gcd0Gcd'15(Succ(Zero), Succ(Succ(x59))))
- We consider the chain new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430), new_gcd0Gcd'13(vuv40, vuv41, Zero, Succ(vuv430)) → new_gcd0Gcd'15(Succ(vuv40), vuv41) which results in the following constraint:
(9) (new_gcd0Gcd'13(x67, x68, x69, x70)=new_gcd0Gcd'13(x71, x72, Zero, Succ(x73)) ⇒ new_gcd0Gcd'13(x71, x72, Zero, Succ(x73))≥new_gcd0Gcd'15(Succ(x71), x72))
We simplified constraint (9) using rules (I), (II), (III) which results in the following new constraint:
(10) (new_gcd0Gcd'13(x67, x68, Zero, Succ(x73))≥new_gcd0Gcd'15(Succ(x67), x68))
For Pair new_gcd0Gcd'15(vuv29, vuv30) → new_gcd0Gcd'17(Succ(vuv30), vuv29, Succ(vuv30)) the following chains were created:
- We consider the chain new_gcd0Gcd'13(vuv40, vuv41, Zero, Succ(vuv430)) → new_gcd0Gcd'15(Succ(vuv40), vuv41), new_gcd0Gcd'15(vuv29, vuv30) → new_gcd0Gcd'17(Succ(vuv30), vuv29, Succ(vuv30)) which results in the following constraint:
(11) (new_gcd0Gcd'15(Succ(x85), x86)=new_gcd0Gcd'15(x88, x89) ⇒ new_gcd0Gcd'15(x88, x89)≥new_gcd0Gcd'17(Succ(x89), x88, Succ(x89)))
We simplified constraint (11) using rules (I), (II), (III) which results in the following new constraint:
(12) (new_gcd0Gcd'15(Succ(x85), x86)≥new_gcd0Gcd'17(Succ(x86), Succ(x85), Succ(x86)))
For Pair new_gcd0Gcd'12(Succ(z0), Neg(Succ(z1))) → new_gcd0Gcd'0(Neg(Succ(z1)), Succ(z0)) the following chains were created:
- We consider the chain new_gcd0Gcd'18(vuv78, vuv79, Zero, Succ(vuv810)) → new_gcd0Gcd'12(Succ(vuv78), Neg(Succ(vuv79))), new_gcd0Gcd'12(Succ(z0), Neg(Succ(z1))) → new_gcd0Gcd'0(Neg(Succ(z1)), Succ(z0)) which results in the following constraint:
(13) (new_gcd0Gcd'12(Succ(x104), Neg(Succ(x105)))=new_gcd0Gcd'12(Succ(x107), Neg(Succ(x108))) ⇒ new_gcd0Gcd'12(Succ(x107), Neg(Succ(x108)))≥new_gcd0Gcd'0(Neg(Succ(x108)), Succ(x107)))
We simplified constraint (13) using rules (I), (II), (III) which results in the following new constraint:
(14) (new_gcd0Gcd'12(Succ(x104), Neg(Succ(x105)))≥new_gcd0Gcd'0(Neg(Succ(x105)), Succ(x104)))
For Pair new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430) the following chains were created:
- We consider the chain new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000), new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430) which results in the following constraint:
(15) (new_gcd0Gcd'13(x131, Succ(x132), x131, x132)=new_gcd0Gcd'13(x133, x134, Succ(x135), Succ(x136)) ⇒ new_gcd0Gcd'13(x133, x134, Succ(x135), Succ(x136))≥new_gcd0Gcd'13(x133, x134, x135, x136))
We simplified constraint (15) using rules (I), (II), (III) which results in the following new constraint:
(16) (new_gcd0Gcd'13(Succ(x135), Succ(Succ(x136)), Succ(x135), Succ(x136))≥new_gcd0Gcd'13(Succ(x135), Succ(Succ(x136)), x135, x136))
- We consider the chain new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430), new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430) which results in the following constraint:
(17) (new_gcd0Gcd'13(x144, x145, x146, x147)=new_gcd0Gcd'13(x148, x149, Succ(x150), Succ(x151)) ⇒ new_gcd0Gcd'13(x148, x149, Succ(x150), Succ(x151))≥new_gcd0Gcd'13(x148, x149, x150, x151))
We simplified constraint (17) using rules (I), (II), (III) which results in the following new constraint:
(18) (new_gcd0Gcd'13(x144, x145, Succ(x150), Succ(x151))≥new_gcd0Gcd'13(x144, x145, x150, x151))
For Pair new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810) the following chains were created:
- We consider the chain new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810), new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810) which results in the following constraint:
(19) (new_gcd0Gcd'18(x174, x175, x176, x177)=new_gcd0Gcd'18(x178, x179, Succ(x180), Succ(x181)) ⇒ new_gcd0Gcd'18(x178, x179, Succ(x180), Succ(x181))≥new_gcd0Gcd'18(x178, x179, x180, x181))
We simplified constraint (19) using rules (I), (II), (III) which results in the following new constraint:
(20) (new_gcd0Gcd'18(x174, x175, Succ(x180), Succ(x181))≥new_gcd0Gcd'18(x174, x175, x180, x181))
- We consider the chain new_gcd0Gcd'17(Succ(Succ(x0)), Succ(x1), Succ(Succ(x0))) → new_gcd0Gcd'18(x0, Succ(x1), x0, x1), new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810) which results in the following constraint:
(21) (new_gcd0Gcd'18(x182, Succ(x183), x182, x183)=new_gcd0Gcd'18(x184, x185, Succ(x186), Succ(x187)) ⇒ new_gcd0Gcd'18(x184, x185, Succ(x186), Succ(x187))≥new_gcd0Gcd'18(x184, x185, x186, x187))
We simplified constraint (21) using rules (I), (II), (III) which results in the following new constraint:
(22) (new_gcd0Gcd'18(Succ(x186), Succ(Succ(x187)), Succ(x186), Succ(x187))≥new_gcd0Gcd'18(Succ(x186), Succ(Succ(x187)), x186, x187))
For Pair new_gcd0Gcd'17(Succ(Succ(x0)), Succ(x1), Succ(Succ(x0))) → new_gcd0Gcd'18(x0, Succ(x1), x0, x1) the following chains were created:
- We consider the chain new_gcd0Gcd'15(vuv29, vuv30) → new_gcd0Gcd'17(Succ(vuv30), vuv29, Succ(vuv30)), new_gcd0Gcd'17(Succ(Succ(x0)), Succ(x1), Succ(Succ(x0))) → new_gcd0Gcd'18(x0, Succ(x1), x0, x1) which results in the following constraint:
(23) (new_gcd0Gcd'17(Succ(x197), x196, Succ(x197))=new_gcd0Gcd'17(Succ(Succ(x198)), Succ(x199), Succ(Succ(x198))) ⇒ new_gcd0Gcd'17(Succ(Succ(x198)), Succ(x199), Succ(Succ(x198)))≥new_gcd0Gcd'18(x198, Succ(x199), x198, x199))
We simplified constraint (23) using rules (I), (II), (III) which results in the following new constraint:
(24) (new_gcd0Gcd'17(Succ(Succ(x198)), Succ(x199), Succ(Succ(x198)))≥new_gcd0Gcd'18(x198, Succ(x199), x198, x199))
To summarize, we get the following constraints P≥ for the following pairs.
- new_gcd0Gcd'18(vuv78, vuv79, Zero, Succ(vuv810)) → new_gcd0Gcd'12(Succ(vuv78), Neg(Succ(vuv79)))
- (new_gcd0Gcd'18(x16, x17, Zero, Succ(x22))≥new_gcd0Gcd'12(Succ(x16), Neg(Succ(x17))))
- (new_gcd0Gcd'18(Zero, Succ(Succ(x27)), Zero, Succ(x27))≥new_gcd0Gcd'12(Succ(Zero), Neg(Succ(Succ(Succ(x27))))))
- new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
- (new_gcd0Gcd'0(Neg(Succ(Succ(x40))), Succ(x38))≥new_gcd0Gcd'13(x40, Succ(x38), x40, x38))
- new_gcd0Gcd'13(vuv40, vuv41, Zero, Succ(vuv430)) → new_gcd0Gcd'15(Succ(vuv40), vuv41)
- (new_gcd0Gcd'13(Zero, Succ(Succ(x59)), Zero, Succ(x59))≥new_gcd0Gcd'15(Succ(Zero), Succ(Succ(x59))))
- (new_gcd0Gcd'13(x67, x68, Zero, Succ(x73))≥new_gcd0Gcd'15(Succ(x67), x68))
- new_gcd0Gcd'15(vuv29, vuv30) → new_gcd0Gcd'17(Succ(vuv30), vuv29, Succ(vuv30))
- (new_gcd0Gcd'15(Succ(x85), x86)≥new_gcd0Gcd'17(Succ(x86), Succ(x85), Succ(x86)))
- new_gcd0Gcd'12(Succ(z0), Neg(Succ(z1))) → new_gcd0Gcd'0(Neg(Succ(z1)), Succ(z0))
- (new_gcd0Gcd'12(Succ(x104), Neg(Succ(x105)))≥new_gcd0Gcd'0(Neg(Succ(x105)), Succ(x104)))
- new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430)
- (new_gcd0Gcd'13(Succ(x135), Succ(Succ(x136)), Succ(x135), Succ(x136))≥new_gcd0Gcd'13(Succ(x135), Succ(Succ(x136)), x135, x136))
- (new_gcd0Gcd'13(x144, x145, Succ(x150), Succ(x151))≥new_gcd0Gcd'13(x144, x145, x150, x151))
- new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810)
- (new_gcd0Gcd'18(x174, x175, Succ(x180), Succ(x181))≥new_gcd0Gcd'18(x174, x175, x180, x181))
- (new_gcd0Gcd'18(Succ(x186), Succ(Succ(x187)), Succ(x186), Succ(x187))≥new_gcd0Gcd'18(Succ(x186), Succ(Succ(x187)), x186, x187))
- new_gcd0Gcd'17(Succ(Succ(x0)), Succ(x1), Succ(Succ(x0))) → new_gcd0Gcd'18(x0, Succ(x1), x0, x1)
- (new_gcd0Gcd'17(Succ(Succ(x198)), Succ(x199), Succ(Succ(x198)))≥new_gcd0Gcd'18(x198, Succ(x199), x198, x199))
The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation [18]:
POL(Neg(x1)) = 0
POL(Succ(x1)) = 1 + x1
POL(Zero) = 0
POL(c) = -1
POL(new_gcd0Gcd'0(x1, x2)) = -1 - x1
POL(new_gcd0Gcd'12(x1, x2)) = -1 - x2
POL(new_gcd0Gcd'13(x1, x2, x3, x4)) = x1 - x2 - x3 + x4
POL(new_gcd0Gcd'15(x1, x2)) = -1 + x1 - x2
POL(new_gcd0Gcd'17(x1, x2, x3)) = -x1 + x2
POL(new_gcd0Gcd'18(x1, x2, x3, x4)) = -1 - x3 + x4
The following pairs are in P>:
new_gcd0Gcd'18(vuv78, vuv79, Zero, Succ(vuv810)) → new_gcd0Gcd'12(Succ(vuv78), Neg(Succ(vuv79)))
new_gcd0Gcd'13(vuv40, vuv41, Zero, Succ(vuv430)) → new_gcd0Gcd'15(Succ(vuv40), vuv41)
The following pairs are in Pbound:
new_gcd0Gcd'18(vuv78, vuv79, Zero, Succ(vuv810)) → new_gcd0Gcd'12(Succ(vuv78), Neg(Succ(vuv79)))
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'12(Succ(z0), Neg(Succ(z1))) → new_gcd0Gcd'0(Neg(Succ(z1)), Succ(z0))
There are no usable rules
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ NonInfProof
↳ AND
↳ QDP
↳ DependencyGraphProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'0(Neg(Succ(Succ(vuv6000))), Succ(vuv4000)) → new_gcd0Gcd'13(vuv6000, Succ(vuv4000), vuv6000, vuv4000)
new_gcd0Gcd'15(vuv29, vuv30) → new_gcd0Gcd'17(Succ(vuv30), vuv29, Succ(vuv30))
new_gcd0Gcd'17(Succ(Succ(x0)), Succ(x1), Succ(Succ(x0))) → new_gcd0Gcd'18(x0, Succ(x1), x0, x1)
new_gcd0Gcd'12(Succ(z0), Neg(Succ(z1))) → new_gcd0Gcd'0(Neg(Succ(z1)), Succ(z0))
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 4 less nodes.
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ NonInfProof
↳ AND
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ NonInfProof
↳ AND
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ NonInfProof
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'13(vuv40, vuv41, Zero, Succ(vuv430)) → new_gcd0Gcd'15(Succ(vuv40), vuv41)
new_gcd0Gcd'15(vuv29, vuv30) → new_gcd0Gcd'17(Succ(vuv30), vuv29, Succ(vuv30))
new_gcd0Gcd'17(Succ(Succ(x0)), Succ(x1), Succ(Succ(x0))) → new_gcd0Gcd'18(x0, Succ(x1), x0, x1)
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430)
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 3 less nodes.
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ NonInfProof
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_gcd0Gcd'18(vuv78, vuv79, Succ(vuv800), Succ(vuv810)) → new_gcd0Gcd'18(vuv78, vuv79, vuv800, vuv810)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ NonInfProof
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_gcd0Gcd'13(vuv40, vuv41, Succ(vuv420), Succ(vuv430)) → new_gcd0Gcd'13(vuv40, vuv41, vuv420, vuv430)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4